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