induction sz <;> intros n <;> cases n <;> simp
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n ≥ 0
case succ.next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
n_ih✝ : ∀ {n : FinInt (Nat.add n✝ 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next a✝¹ a✝)