rw [List.reduceOption_mem_iff]
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✝
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ some 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✝ ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝