all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [⊥], none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝, ~φ✝], none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~~φ✝], none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝⋀ψ✝], none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~φ✝⋀ψ✝], none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [⌈α✝⌉φ✝], none), y < x

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 neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)

case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

case nCo
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 χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

case box
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 ∈ unfoldBox α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < lmOfProgram α✝ + lmOfFormula φ✝

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 φ✝)