rw [h] at h₁
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (addfull n m) = toUint n + toUint m
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz