. simp [FinInt.addfull_toUint] at h₂
  rw [h₂] at h_bound
  sorry_arith
case true
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next true r
h₂ : toUint (addfull n m) = 2 ^ sz + toUint r
⊢ toUint
      (match next true r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
no goals