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