Proof step 4 from proof butmin-rewput (previous step)

⊦ a = st[a, d].min, ∀ a0. (a0 ∈ st[a, d] -- st[a, d].min ↔ a0 ∈ (st -- st.min)[a, d]) ∧ (st[a, d] -- st[a, d].min)[a0] = (st -- st.min)[a, d][a0]

Heuristic simplifier applied rule simplifier

Proof step 5:
⊦ a = st[a, d].min, (a0 ∈ st[a, d] -- st[a, d].min ↔ a0 ∈ (st -- st.min)[a, d]) ∧ (st[a, d] -- st[a, d].min)[a0] = (st -- st.min)[a, d][a0]