cases rule
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
X : List TNode
rule : LocalRule (Lcond, Rcond, Ocond) X
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ node_to_multiset (Lcond, ∅, none) ≠ ∅

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ node_to_multiset (∅, Rcond, none) ≠ ∅

case LRnegL
ϕ✝ : Formula
⊢ node_to_multiset ([ϕ✝], [~ϕ✝], none) ≠ ∅

case LRnegR
ϕ✝ : Formula
⊢ node_to_multiset ([~ϕ✝], [ϕ✝], none) ≠ ∅

case loadedL
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))) ≠ ∅

case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅