have h₂: (addfull n m).toUint = (next carry r).toUint := by simp [h₁]
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
h₂ : toUint (addfull n m) = toUint (next carry r)
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)