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

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)
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)