cases h_full: addfull n m
sz : ℕ
n m : FinInt sz
⊢ (match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
case next
sz : ℕ
n m : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
h_full : addfull n m = next a✝¹ a✝
⊢ (match next a✝¹ a✝ with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz