Theorem: unfoldDiamond.decreases_lmOf (Pdl/LocalTableau.lean)

State before:
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_E : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
Tactic:
sorry
State after:
no goals