exact unfoldDiamond.decreases_lmOf E_in y_in_Y
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
no goals