Proof step 9 from proof perm-last-rec (previous step)
perm(x -1l a0, y0 + a ') ↔ a ∈ x -1l a0 ∧ perm((x -1l a0) -1l a, y0)
⊦ a0 ∈ x ∧ perm(x -1l a0, y0 + a ') ↔ a ∈ x ∧ a0 ∈ x -1l a ∧ perm((x -1l a0) -1l a, y0)
User applied rule cut formula
And closed the goal!
Rule argument
fma: a = a0
Additional information
Used simplifier rules:
⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x); (s)
Used formulas: a = a0