intro x
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ ∀ (x : Fin (N + 1) → Bool),
    (match x 0 with
      | false => g (Fin.cons false (Fin.tail x))
      | true => g (Fin.cons true (Fin.tail x))) =
      g x
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
⊢ (match x 0 with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x