rw [Finset.insert_eq_of_mem in_x]
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOfSet X ≤ lengthOfSet X + lengthOfFormula ϕ