Proof step 8 from proof inj-put (previous step)

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

Heuristic simplifier applied rule simplifier

Proof step 9:
∀ a0. (a0 ∈ st[a, d] ↔ a0 ∈ st0[a, d]) ∧ st[a, d][a0] = st0[a, d][a0] ⊦ a ∈ st, a ∈ st0, (a0 ∈ st ↔ a0 ∈ st0) ∧ st[a0] = st0[a0]