Proof step 4 from proof ext-rec (previous step)

a ∈ st1 ∧ st1[a] = d ∧ (∀ b. a ≠ b → (b ∈ st0 ↔ b ∈ st1) ∧ (b ∈ st0 → st0[b] = st1[b])) ⊦ ∀ a0. (a0 ∈ st1 ↔ a0 ∈ st0[a, d]) ∧ st1[a0] = st0[a, d][a0]

Heuristic simplifier applied rule simplifier

Proof step 5:
a ∈ st1, ∀ b. a ≠ b → (b ∈ st0 ↔ b ∈ st1) ∧ (b ∈ st0 → st0[b] = st1[b]) ⊦ (a0 ∈ st1 ↔ a0 ∈ st0[a, st1[a]]) ∧ st1[a0] = st0[a, st1[a]][a0]