subst E_def
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)