cases h₁: addfull n m
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint
      (match addfull n m with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
case next
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
a✝¹ : Bool
a✝ : FinInt sz
h₁ : addfull n m = next a✝¹ a✝
⊢ toUint
      (match next a✝¹ a✝ with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)