have ℓ_left := (Finset.mem_inter.mp ℓ_in_proj).left
case 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
⊢ ℓ ∈ voc (L, R).1
case 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
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1