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