subst_eqs
case inr
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
h✝ : Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([~ψ✝], [], 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 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)