subst_eqs
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = (~ψ✝)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
case inr.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula (~ψ✝) < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)