constructor
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
case val
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ LocalTableau LR