unfold jvoc at *
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inl φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)
φ : 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
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2