rcases canApplyRule with ⟨LCond, RCond, C, lr_exists, preconL, preconR⟩
LR : TNode
canApplyRule : ∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
case intro.intro.intro.intro.intro
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
lr_exists : Nonempty (LocalRule (LCond, RCond) C)
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)