simp [Nat.ofBits]
case h
hd tl : Memory
xs : List Bool
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) xs = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) xs
case h
hd tl : Memory
xs : List Bool
⊢ Nat.bit (Memory.getv hd) (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat (Memory.getv hd)