apply ih
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ ?f.true.a.b

case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ?f.true.a.b ≤ n + n

case f.true.a.b
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ℕ

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

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