match n with
| .O m => simp [toSint, toUint]
| .I m => simp [toSint, toUint]; sorry_arith
sz : ℕ
n : FinInt (sz + 1)
⊢ toSint n =
    match n with
    | next false a => toUint n
    | next true a => toUint n - 2 ^ (sz + 1)
no goals