cases rule
<;> (simp at *; try rw [in_ress])
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~rule} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {rule} ∧ res.1 = ∅
no goals