case nil =>
  simp only [projection, formProjection, beq_iff_eq, List.map_nil, List.not_mem_nil, iff_false]
  exact List.count_eq_zero.mp rfl
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []
no goals