match HMem.Memory.getv hd with
| true => simp [← Nat.two_mul]
| false => simp [← Nat.two_mul]
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)
no goals