rw [h'] at h
sz : ℕ
n' m' : FinInt sz
h :
  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')
br : Bool
r : FinInt sz
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r 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')
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)