simp [node_to_multiset] at *
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([~⌈α✝⌉φ✝], ∅, none), y < x
case dia
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
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)