have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) i = decide (succ k = succ i)
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
this : k = i ↔ succ k = succ i
⊢ getBit (2 ^ k) i = decide (succ k = succ i)