case box β φ =>
  cases β
  case star β =>
    simp
    sorry
  all_goals sorry
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
β : Program
φ : Formula
y_in_E : (⌈β⌉φ) ∈ E
⊢ lmOfFormula (⌈β⌉φ) < lmOfProgram α + lmOfFormula φ✝
no goals