case next bn n' =>
cases m; case next bm m' =>
cases bn <;> cases bm <;> simp [addfull] at *
case false.false =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, toSint] at * <;> sorry_arith
case false.true =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
case true.false =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
case true.true =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, toSint] at * <;> sorry_arith
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
h :
  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
⊢ toSint (next bn n' + m) =
    match next bn n', m with
    | next false n'_1, next false m' =>
      match next bn n' + m with
      | next false a => toSint (next bn n') + toSint m
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next bn n') + toSint m
    | next true n'_1, next false m' => toSint (next bn n') + toSint m
    | next true n'_1, next true m' =>
      match 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
no goals