cases b <;> simp [-Nat.bit_false, -Nat.bit_true, Nat.bit_mod_two, Nat.bit_div_2]
case hi.h₂.right
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 b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
case hi.h₂.right.false
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → false = true
⊢ encodeList (Nat.bits n) = encode n

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