cases f
f : Formula
⊢ (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f
case bottom

⊢ (projection {bottom}).sum lengthOfFormula ≤ lengthOfFormula bottom

case atom_prop
a✝ : Char
⊢ (projection {·a✝}).sum lengthOfFormula ≤ lengthOfFormula (·a✝)

case neg
a✝ : Formula
⊢ (projection {~a✝}).sum lengthOfFormula ≤ lengthOfFormula (~a✝)

case And
a✝¹ a✝ : Formula
⊢ (projection {a✝¹⋀a✝}).sum lengthOfFormula ≤ lengthOfFormula (a✝¹⋀a✝)

case box
a✝ : Formula
⊢ (projection {□a✝}).sum lengthOfFormula ≤ lengthOfFormula (□a✝)