simp only [applyLocalRule, List.mem_map] at c_child
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))
c_child : c ∈ applyLocalRule rule (L, R)
⊢ lengthOfTNode c < lengthOfTNode (L, R)
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))
c_child : ∃ a ∈ ress, (L \ Lcond ∪ a.1, R \ Rcond ∪ a.2) = c
⊢ lengthOfTNode c < lengthOfTNode (L, R)