match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
no goals