cases b
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ succ (size n) ≤ bit b n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ bit false n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0