cases rule
X : TNode
ress : List TNode
rule : LocalRule X ress
Y : TNode
Y_in_ress : Y ∈ ress
y : Formula
y_in_Y : y ∈ node_to_multiset Y
⊢ ∃ x ∈ node_to_multiset X, y < x
case oneSidedL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (precond✝, ∅, none), y < x

case oneSidedR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (∅, precond✝, none), y < x

case LRnegL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x

case LRnegR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x

case loadedL
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.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x

case loadedR
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✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))), y < x