cases bn <;> cases bm <;> rfl
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)
no goals