simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
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✝
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈
      ((match A, head✝ with
          | A, ⌈·B⌉φ => if A = B then some φ else none
          | x, x_1 => none) ::
          List.map
            (fun x =>
              match A, x with
              | A, ⌈·B⌉φ => if A = B then some φ else none
              | x, x_1 => none)
            tail✝).reduceOption ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝