simpa using λ h ↦ absurd (hb h) Bool.noConfusion
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ bit false n ≠ 0

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