cases m
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
⊢ toSint (addfull (next bn n') m) =
    match next bn n', m with
    | next false n'_1, next false m' => toSint (next bn n') + toSint m
    | next false n'_1, next true m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint m
case next
sz : ℕ
bn : Bool
n' : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
⊢ toSint (addfull (next bn n') (next a✝¹ a✝)) =
    match next bn n', next a✝¹ a✝ with
    | next false n'_1, next false m' => toSint (next bn n') + toSint (next a✝¹ a✝)
    | next false n'_1, next true m' =>
      match addfull (next bn n') (next a✝¹ a✝) with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') (next a✝¹ a✝) with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint (next a✝¹ a✝)