cases' em (ϕ ∈ X) with in_x not_in_x
X : Finset Formula
ϕ : Formula
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ

case inr
X : Finset Formula
ϕ : Formula
not_in_x : ϕ ∉ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ