intro c cinC ℓ ℓ_in_c
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
⊢ ∀ cLR ∈ C, jvoc cLR ⊆ jvoc (L, R)
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : ℓ ∈ jvoc c
⊢ ℓ ∈ jvoc (L, R)