- ##[ ##1: #H6; napply (or5_intro1 … H6)
- ##| ##2: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
- ##[ ##1: #H7; napply (or5_intro2 … H7)
- ##| ##2: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
- ##[ ##1: #H8; napply (or5_intro3 … H8)
- ##| ##2: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
- ##[ ##1: #H9; napply (or5_intro4 … H9)
- ##| ##2: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
- ##[ ##1: #H10; napply (or5_intro5 … H10)
- ##| ##2: #H10; nrewrite > H6 in H:(%);
+ ##[ ##2: #H6; napply (or5_intro1 … H6)
+ ##| ##1: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##2: #H7; napply (or5_intro2 … H7)
+ ##| ##1: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##2: #H8; napply (or5_intro3 … H8)
+ ##| ##1: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
+ ##[ ##2: #H9; napply (or5_intro4 … H9)
+ ##| ##1: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
+ ##[ ##2: #H10; napply (or5_intro5 … H10)
+ ##| ##1: #H10; nrewrite > H6 in H:(%);