use ~(□φ)
case a.left
φ : 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
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
case h
φ : 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
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R ∧ ℓ ∈ vocabOfFormula (~(□φ))