have claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ :=
  by
  apply lengthAdd
  simp
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X