Proof step 3 from proof oplus-shift-put-l (previous step)

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

Heuristic simplifier applied rule simplifier

Proof step 4:
⊦ (a0 ∈ st0[a, d] ⊕ st1 ↔ a0 ∈ (st0 ⊕ st1)[a, d]) ∧ (a0 ∈ st0[a, d] ⊕ st1 → (st0[a, d] ⊕ st1)[a0] = (st0 ⊕ st1)[a, d][a0])