intros h <;> induction sz
sz : ℕ
a b : FinInt sz
⊢ toUint a = toUint b → a = b
case zero
a b : FinInt Nat.zero
h : toUint a = toUint b
⊢ a = b

case succ
n✝ : ℕ
n_ih✝ : ∀ (a b : FinInt n✝), toUint a = toUint b → a = b
a b : FinInt (Nat.succ n✝)
h : toUint a = toUint b
⊢ a = b