Proof step 4 from proof del-two (previous step)

a4 ∈ s, a3 ∈ s, a1 ∈ s, ∀ a4. a4 = b ∨ a4 = a ∨ ¬ a4 ∈ s ⊦ a0 ∈ s ↔ a0 ∈ ∅ ++ a ++ b, a1 ∈ s ↔ a1 = b, a2 ∈ s ↔ a2 = a

Heuristic simplifier applied rule simplifier

Proof step 5:
a1 ∈ s, a3 ∈ s, a4 ∈ s, ∀ a4. a4 = b ∨ a4 = a ∨ ¬ a4 ∈ s ⊦ a0 ∈ s ↔ a0 ∈ ∅ ++ a ++ b, a2 ∈ s ↔ a2 = a, a1 = b