match h: addfull n m with
| .next br r =>
  have h₁ := FinInt.addfull_toUint n m
  rw [h] at h₁
  have h₂: n+m = r := by simp [HAdd.hAdd, add, h]
  cases br <;> simp [h₂] at *
  . exact h₁
  . sorry_arith
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) =
    match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
no goals