rw [recBase2_div2, h_ind]
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n + 2) = log2 (n + 2)
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ log2 (n / 2 + 1) + 1 = log2 (n + 2)