conv => change getBit 0 i = false
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit 0 i = false