- napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_w16_aux1 b1 b2 b3 b4 H))
- ##| ##1: #H; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
- ##[ ##2: #H1; napply (or_intror … (decidable_w16_aux2 b1 b2 b3 b4 H1))
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w16_aux1 b1 b2 b3 b4 H))
+ ##| ##1: #H; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_w16_aux2 b1 b2 b3 b4 H1))