cases lS
case intro.intro
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
lS : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
case intro.intro.inl
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
h✝ : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)

case intro.intro.inr
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
h✝ : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)