- napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_w32_aux1 w1 w2 w3 w4 H))
- ##| ##1: #H; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
- ##[ ##2: #H1; napply (or_intror … (decidable_w32_aux2 w1 w2 w3 w4 H1))
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H))
+ ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1))