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