simp at ℓ_in_voc_Rcond
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 : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
ℓ_in_voc_Rcond : ℓ ∈ Rcond.biUnion vocabOfFormula := voc_res_ss_Rcond Rφ Rφ_in_res_R ℓ_in_Rφ
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
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 : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
ℓ_in_voc_Rcond : ∃ a ∈ Rcond, ℓ ∈ vocabOfFormula a
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ