intro ℓ_in_φ
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).1
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).1