intro ⟨ψ, ψ_in_proj, ℓ_in_ψ⟩
case a.right
φ : 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
⊢ (∃ a ∈ projection R, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).2
case a.right
φ : 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 ψ
⊢ ℓ ∈ voc (L, R).2