induction X using Finset.induction_on
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} = X.erase ϕ
case empty
ϕ : Formula
⊢ ∅ \ {ϕ} = ∅.erase ϕ

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ