induction X
g : Formula
A : ℕ
X : List Formula
⊢ g ∈ projection A X ↔ (⌈·A⌉g) ∈ X
case nil
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []

case 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✝