apply LocalRuleApp.mk C LCond RCond lr ⟨preconL, preconR⟩
case intro.intro.intro.intro.intro.intro.val.ruleA
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ LocalRuleApp LR ?intro.intro.intro.intro.intro.intro.val.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 ∈ ?intro.intro.intro.intro.intro.intro.val.C → LocalTableau c

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

LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ ?intro.intro.intro.intro.intro.intro.val.C = applyLocalRule lr (LR.1, LR.2)

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 ∈ ?intro.intro.intro.intro.intro.intro.val.C → LocalTableau c

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