apply congrArg (encode (α := List Bool))
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) = ?hi.b

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ ?hi.b = Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

case hi.b
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Memory
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Nat.bits (Nat.bit b n) = ?m.80295

n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ List Bool

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode ?m.80295 =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))