cases rule
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ {~rule} ∩ res.1 = ∅ ∧ {rule} ∩ res.2 = ∅
case LRnegR.bottom
res : SubPair
in_ress : res ∈ ∅
⊢ {~bottom} ∩ res.1 = ∅ ∧ {bottom} ∩ res.2 = ∅

case LRnegR.atom_prop
res : SubPair
in_ress : res ∈ ∅
a✝ : Char
⊢ {~·a✝} ∩ res.1 = ∅ ∧ {·a✝} ∩ res.2 = ∅

case LRnegR.neg
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~~a✝} ∩ res.1 = ∅ ∧ {~a✝} ∩ res.2 = ∅

case LRnegR.And
res : SubPair
in_ress : res ∈ ∅
a✝¹ a✝ : Formula
⊢ {~(a✝¹⋀a✝)} ∩ res.1 = ∅ ∧ {a✝¹⋀a✝} ∩ res.2 = ∅

case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅