cases m
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + m, false)) =
    match m, next a✝¹ a✝ with
    | next false n', next false m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + next a✝¹ a✝, false)
case next.next
sz : ℕ
a✝³ : Bool
a✝² : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝³ a✝², next a✝¹ a✝ with
    | next false n', next false m' =>
      match next a✝³ a✝² + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝³ a✝² + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝³ a✝² + next a✝¹ a✝, false)) =
    match next a✝¹ a✝, next a✝³ a✝² with
    | next false n', next false m' =>
      match next a✝¹ a✝ + next a✝³ a✝² with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + next a✝³ a✝² with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + next a✝³ a✝², false)