constructor
case intro.intro.intro.intro.intro.intro
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ Nonempty (LocalTableau LR)
case intro.intro.intro.intro.intro.intro.val
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ LocalTableau LR