cases n
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ log 2 n + 1
⊢ size (bit b n) ≤ log 2 (bit b n) + 1
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero ≤ log 2 zero + 1
⊢ size (bit b zero) ≤ log 2 (bit b zero) + 1

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1