use ψ
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
no goals