freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / common / prod_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
index 15afe0a68b8f293a5ae54ae358202317aa266aa5..b73d1347f58269eee3f933bbf74bad840709f49f 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
@@ -118,12 +118,12 @@ nlemma decidable_pair
  #y; nelim y; #yy1; #yy2;
  nnormalize;
  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
           nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
- ##| ##2: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
-          ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+          ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                    nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
-          ##| ##2: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+          ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
                    nrewrite > H2; nrewrite > H3; napply refl_eq
           ##]
  ##]
@@ -143,8 +143,8 @@ nlemma neqpair_to_neq :
  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
  nnormalize; #H3;
  napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
- ##[ ##1: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
- ##| ##2: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
+ ##[ ##1: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
+ ##| ##2: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
  ##]
 nqed.
 
@@ -156,10 +156,10 @@ nlemma pair_destruct
  #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
  nnormalize; #H;
  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H3; napply (or2_intro1 … H3)
- ##| ##2: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
-          ##[ ##1: #H4; napply (or2_intro2 … H4)
-          ##| ##2: #H4; nrewrite > H3 in H:(%);
+ ##[ ##2: #H3; napply (or2_intro1 … H3)
+ ##| ##1: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+          ##[ ##2: #H4; napply (or2_intro2 … H4)
+          ##| ##1: #H4; nrewrite > H3 in H:(%);
                    nrewrite > H4; #H; nelim (H (refl_eq …))
           ##]
  ##]
@@ -180,8 +180,8 @@ nlemma neq_to_neqpair :
  #x2; #y2; #H;
  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
  napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
- ##[ ##1: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
- ##| ##2: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
+ ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
+ ##| ##1: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
  ##]
 nqed.
 
@@ -305,15 +305,15 @@ nlemma decidable_triple
  #y; nelim y; #yy1; #yy2; #yy3;
  nnormalize;
  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
           nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
- ##| ##2: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
-          ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+          ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                    nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
-          ##| ##2: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
-                   ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+          ##| ##1: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+                   ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
-                   ##| ##2: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+                   ##| ##1: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
                             nrewrite > H3;
                             nrewrite > H4;
                             nrewrite > H5;
@@ -338,9 +338,9 @@ nlemma neqtriple_to_neq :
  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
  nnormalize; #H4;
  napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
- ##[ ##1: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
- ##| ##2: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
- ##| ##3: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
+ ##[ ##1: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
+ ##| ##2: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
+ ##| ##3: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
  ##]
 nqed.
 
@@ -354,12 +354,12 @@ nlemma triple_destruct
  #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
  nnormalize; #H;
  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H4; napply (or3_intro1 … H4)
- ##| ##2: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
-          ##[ ##1: #H5; napply (or3_intro2 … H5)
-          ##| ##2: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
-                   ##[ ##1: #H6; napply (or3_intro3 … H6)
-                   ##| ##2: #H6; nrewrite > H4 in H:(%);
+ ##[ ##2: #H4; napply (or3_intro1 … H4)
+ ##| ##1: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+          ##[ ##2: #H5; napply (or3_intro2 … H5)
+          ##| ##1: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+                   ##[ ##2: #H6; napply (or3_intro3 … H6)
+                   ##| ##1: #H6; nrewrite > H4 in H:(%);
                             nrewrite > H5;
                             nrewrite > H6; #H; nelim (H (refl_eq …))
                    ##]
@@ -384,9 +384,9 @@ nlemma neq_to_neqtriple :
  #x2; #y2; #z2; #H;
  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
  napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
- ##[ ##1: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
- ##| ##2: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
- ##| ##3: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
+ ##[ ##1: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
+ ##| ##2: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
+ ##| ##3: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
  ##]
 nqed.
 
@@ -536,18 +536,18 @@ nlemma decidable_quadruple
  #y; nelim y; #yy1; #yy2; #yy3; #yy4;
  nnormalize;
  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
           nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
- ##| ##2: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
-          ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+          ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                    nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
-          ##| ##2: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
-                   ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+          ##| ##1: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+                   ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
-                   ##| ##2: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
-                            ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                   ##| ##1: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
+                            ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                                      nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
-                            ##| ##2: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+                            ##| ##1: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
                                      nrewrite > H4;
                                      nrewrite > H5;
                                      nrewrite > H6;
@@ -575,10 +575,10 @@ nlemma neqquadruple_to_neq :
  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
  nnormalize; #H5;
  napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
- ##[ ##1: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
- ##| ##2: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
- ##| ##3: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
- ##| ##4: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
+ ##[ ##1: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
+ ##| ##2: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
+ ##| ##3: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
+ ##| ##4: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
  ##]
 nqed.
 
@@ -595,14 +595,14 @@ nlemma quadruple_destruct
  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
  nnormalize; #H;
  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H5; napply (or4_intro1 … H5)
- ##| ##2: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
-          ##[ ##1: #H6; napply (or4_intro2 … H6)
-          ##| ##2: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
-                   ##[ ##1: #H7; napply (or4_intro3 … H7)
-                   ##| ##2: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
-                            ##[ ##1: #H8; napply (or4_intro4 … H8)
-                            ##| ##2: #H8; nrewrite > H5 in H:(%);
+ ##[ ##2: #H5; napply (or4_intro1 … H5)
+ ##| ##1: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+          ##[ ##2: #H6; napply (or4_intro2 … H6)
+          ##| ##1: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+                   ##[ ##2: #H7; napply (or4_intro3 … H7)
+                   ##| ##1: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
+                            ##[ ##2: #H8; napply (or4_intro4 … H8)
+                            ##| ##1: #H8; nrewrite > H5 in H:(%);
                                      nrewrite > H6;
                                      nrewrite > H7;
                                      nrewrite > H8; #H; nelim (H (refl_eq …))
@@ -631,10 +631,10 @@ nlemma neq_to_neqquadruple :
  #x2; #y2; #z2; #v2; #H;
  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
  napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
- ##[ ##1: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
- ##| ##2: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
- ##| ##3: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
- ##| ##4: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##[ ##1: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##| ##2: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##| ##3: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
+ ##| ##4: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
  ##]
 nqed.
 
@@ -810,21 +810,21 @@ nlemma decidable_quintuple
  #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
  nnormalize;
  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
           nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
- ##| ##2: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
-          ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+          ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                    nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
-          ##| ##2: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
-                   ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+          ##| ##1: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+                   ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
-                   ##| ##2: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
-                            ##[ ##1: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                   ##| ##1: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
+                            ##[ ##2: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                                      nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
-                            ##| ##2: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
-                                     ##[ ##1: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                            ##| ##1: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
+                                     ##[ ##2: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                                               nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
-                                     ##| ##2: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+                                     ##| ##1: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
                                               nrewrite > H5;
                                               nrewrite > H6;
                                               nrewrite > H7;
@@ -855,11 +855,11 @@ nlemma neqquintuple_to_neq :
  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
  nnormalize; #H6;
  napply (or5_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ((f5 w1 w2) = false) ? (andb_false5 … H) ?);
- ##[ ##1: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
- ##| ##2: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
- ##| ##3: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
- ##| ##4: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
- ##| ##5: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
+ ##[ ##1: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
+ ##| ##2: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
+ ##| ##3: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
+ ##| ##4: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
+ ##| ##5: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
  ##]
 nqed.
 
@@ -877,16 +877,16 @@ nlemma quintuple_destruct
  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
  nnormalize; #H;
  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##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:(%);
                                               nrewrite > H7;
                                               nrewrite > H8;
                                               nrewrite > H9;
@@ -921,10 +921,10 @@ nlemma neq_to_neqquintuple :
  #x2; #y2; #z2; #v2; #w2; #H;
  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
  napply (or5_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2) ? (quintuple_destruct T1 T2 T3 T4 T5 H1 H2 H3 H4 H5 … H) ?);
- ##[ ##1: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
- ##| ##2: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
- ##| ##3: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
- ##| ##4: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
- ##| ##5: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##[ ##1: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##2: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##3: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##4: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
+ ##| ##5: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
  ##]
 nqed.