cases k
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k / 2) i = decide (k = succ i)
case zero
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)

case succ
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
n✝ : Nat
⊢ getBit (2 ^ succ n✝ / 2) i = decide (succ n✝ = succ i)