cases lrule
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))