apply Or.elim (em (Lφ ∈ L))
case left
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
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
case left.left
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
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ Lφ ∈ L → ∃ a ∈ L, ℓ ∈ vocabOfFormula a

case left.right
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
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ Lφ ∉ L → ∃ a ∈ L, ℓ ∈ vocabOfFormula a