case cons =>
  simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
  rw [List.reduceOption_mem_iff]
  aesop
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝
no goals