intro c c_in
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ applyLocalRule lr (LR.1, LR.2) → LocalTableau c
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
⊢ LocalTableau c