cases bn <;> simp [@ih n']
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next bn n')
case true
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ 2 ^ sz + toUint n'