let ⟨ress, Lcond, Rcond, rule, precondProofL, precondProofR⟩ := lrApp
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
⊢ lengthOfTNode c < lengthOfTNode (L, R)
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC✝ : C = applyLocalRule rule (L, R)
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
⊢ lengthOfTNode c < lengthOfTNode (L, R)