induction X using Finset.induction_on
X : Finset Formula
⊢ lengthOfSet (projection X) ≤ lengthOfSet X
case empty

⊢ lengthOfSet (projection ∅) ≤ lengthOfSet ∅

case insert
a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : lengthOfSet (projection s✝) ≤ lengthOfSet s✝
⊢ lengthOfSet (projection (insert a✝² s✝)) ≤ lengthOfSet (insert a✝² s✝)