cases' em (φ = ψ) with heq hneq
φ ψ : Formula
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
case inl
φ ψ : Formula
heq : φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ

case inr
φ ψ : Formula
hneq : ¬φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ