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