all_goals sorry
case bottom
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_E : Formula.bottom ∈ E
⊢ lmOfFormula Formula.bottom < lmOfProgram α + lmOfFormula φ

case atom_prop
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝ : ℕ
y_in_E : (·a✝) ∈ E
⊢ lmOfFormula (·a✝) < lmOfProgram α + lmOfFormula φ

case neg
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝ : Formula
y_in_E : (~a✝) ∈ E
⊢ lmOfFormula (~a✝) < lmOfProgram α + lmOfFormula φ

case and
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝¹ a✝ : Formula
y_in_E : a✝¹⋀a✝ ∈ E
⊢ lmOfFormula (a✝¹⋀a✝) < lmOfProgram α + lmOfFormula φ
no goals