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