simp [HAdd.hAdd, FinInt.add, FinInt.addfull_toUint]
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint (n + m) = toUint n + toUint m
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint
      (match addfull n m with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)