Release 0.5.9.

[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 79863d9a01586d7f6ca7f7effa1d542a785bd8d5..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
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -48,15 +48,16 @@ nlemma pair_destruct_2 :
 nqed.
 
 nlemma symmetric_eqpair :
-∀T1,T2:Type.
+∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (symmetricT T1 bool f1) →
  (symmetricT T2 bool f2) →
- (∀p1,p2:ProdT T1 T2. 
-  (eq_pair T1 T2 f1 f2 p1 p2 = eq_pair T1 T2 f1 f2 p1 p2)).
- #T1; #T2; #f1; #f2; #H; #H1;
- #p1; nelim p1; #x1; #y1;
- #p2; nelim p2; #x2; #y2;
+ (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2;
  nnormalize;
  nrewrite > (H x1 x2);
  ncases (f1 x2 x1);
@@ -67,15 +68,16 @@ nlemma symmetric_eqpair :
 nqed.
 
 nlemma eq_to_eqpair :
-∀T1,T2.
+∀T1,T2.∀p1,p2:ProdT T1 T2.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (∀x,y:T1.x = y → f1 x y = true) →
  (∀x,y:T2.x = y → f2 x y = true) →
- (∀p1,p2:ProdT T1 T2.
-   (p1 = p2 → eq_pair T1 T2 f1 f2 p1 p2 = true)).
- #T1; #T2; #f1; #f2; #H1; #H2;
- #p1; nelim p1; #x1; #y1;
- #p2; nelim p2; #x2; #y2; #H;
+ (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2; #H;
  nnormalize;
  nrewrite > (H1 … (pair_destruct_1 … H));
  nnormalize;
@@ -84,32 +86,33 @@ nlemma eq_to_eqpair :
 nqed.
 
 nlemma eqpair_to_eq :
-∀T1,T2.
+∀T1,T2.∀p1,p2:ProdT T1 T2.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (∀x,y:T1.f1 x y = true → x = y) →
  (∀x,y:T2.f2 x y = true → x = y) →
- (∀p1,p2:ProdT T1 T2. 
-  (eq_pair T1 T2 f1 f2 p1 p2 = true → p1 = p2)).
- #T1; #T2; #f1; #f2; #H1; #H2;
- #p1; nelim p1; #x1; #y1;
- #p2; nelim p2; #x2; #y2; #H;
+ (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
  #H3;
- ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
+ ##[ ##2: napply (bool_destruct … H3) ##]
  #H4;
  nrewrite > (H4 (refl_eq …));
  nrewrite > (H2 y1 y2 H3);
  napply refl_eq.
 nqed.
 
-nlemma decidable_pair :
-∀T1,T2.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:ProdT T1 T2.decidable (x = y)).
+nlemma decidable_pair
+ : ∀T1,T2.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   ∀x,y:ProdT T1 T2.decidable (x = y).
  #T1; #T2; #H; #H1;
  #x; nelim x; #xx1; #xx2;
  #y; nelim y; #yy1; #yy2;
@@ -127,15 +130,16 @@ nlemma decidable_pair :
 nqed.
 
 nlemma neqpair_to_neq :
-∀T1,T2.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ ∀T1,T2.∀p1,p2:ProdT T1 T2.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (∀x,y:T1.f1 x y = false → x ≠ y) →
  (∀x,y:T2.f2 x y = false → x ≠ y) →
- (∀p1,p2:ProdT T1 T2.  
-  (eq_pair T1 T2 f1 f2 p1 p2 = false → p1 ≠ p2)).
- #T1; #T2; #f1; #f2; #H1; #H2;
- #p1; nelim p1; #x1; #y1;
- #p2; nelim p2; #x2; #y2;
+ (eq_pair T1 T2 p1 p2 f1 f2 = false → p1 ≠ p2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2;
  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) ?);
@@ -144,12 +148,11 @@ nlemma neqpair_to_neq :
  ##]
 nqed.
 
-nlemma pair_destruct :
-∀T1,T2.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x1,x2:T1.∀y1,y2:T2.
-  (pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2).
+nlemma pair_destruct
+ : ∀T1,T2.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   ∀x1,x2:T1.∀y1,y2:T2.(pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2.
  #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
  nnormalize; #H;
  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
@@ -163,17 +166,18 @@ nlemma pair_destruct :
 nqed.
 
 nlemma neq_to_neqpair :
-∀T1,T2.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ ∀T1,T2.∀p1,p2:ProdT T1 T2.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (∀x,y:T1.decidable (x = y)) →
  (∀x,y:T2.decidable (x = y)) →
  (∀x,y:T1.x ≠ y → f1 x y = false) →
  (∀x,y:T2.x ≠ y → f2 x y = false) →
- (∀p1,p2:ProdT T1 T2. 
-  (p1 ≠ p2 → eq_pair T1 T2 f1 f2 p1 p2 = false)).
- #T1; #T2; #f1; #f2; #H1; #H2; #H3; #H4;
- #p1; nelim p1; #x1; #y1;
- #p2; nelim p2; #x2; #y2; #H;
+ (p1 ≠ p2 → eq_pair T1 T2 p1 p2 f1 f2 = false).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #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) ?);
  ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
@@ -216,16 +220,17 @@ nlemma triple_destruct_3 :
 nqed.
 
 nlemma symmetric_eqtriple :
-∀T1,T2,T3:Type.
+∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (symmetricT T1 bool f1) →
  (symmetricT T2 bool f2) →
  (symmetricT T3 bool f3) →
- (∀p1,p2:Prod3T T1 T2 T3.
-  (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = eq_triple T1 T2 T3 f1 f2 f3 p2 p1)).
- #T1; #T2; #T3; #f1; #f2; #f3; #H; #H1; #H2;
- #p1; nelim p1; #x1; #y1; #z1;
- #p2; nelim p2; #x2; #y2; #z2;
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2;
  nnormalize;
  nrewrite > (H x1 x2);
  ncases (f1 x2 x1);
@@ -241,16 +246,17 @@ nlemma symmetric_eqtriple :
 nqed.
 
 nlemma eq_to_eqtriple :
-∀T1,T2,T3.
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
- (∀p1,p2:Prod3T T1 T2 T3.
-  (p1 = p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true)).
- #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
- #p1; nelim p1; #x1; #y1; #z1;
- #p2; nelim p2; #x2; #y2; #z2; #H;
+ (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2; #H;
  nnormalize;
  nrewrite > (H1 … (triple_destruct_1 … H));
  nnormalize;
@@ -261,25 +267,26 @@ nlemma eq_to_eqtriple :
 nqed.
 
 nlemma eqtriple_to_eq :
-∀T1,T2,T3.
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
- (∀p1,p2:Prod3T T1 T2 T3.
-  (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true → p1 = p2)).
- #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
- #p1; nelim p1; #x1; #y1; #z1;
- #p2; nelim p2; #x2; #y2; #z2; #H;
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
+ ##[ ##2: #H4; napply (bool_destruct … H4) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
+ ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
  #H4; #H5; #H6;
  nrewrite > (H4 (refl_eq …));
  nrewrite > (H6 (refl_eq …));
@@ -287,12 +294,12 @@ nlemma eqtriple_to_eq :
  napply refl_eq.
 nqed.
 
-nlemma decidable_triple :
-∀T1,T2,T3.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:T3.decidable (x = y)) →
- (∀x,y:Prod3T T1 T2 T3.decidable (x = y)).
+nlemma decidable_triple
+ : ∀T1,T2,T3.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   (∀x,y:T3.decidable (x = y)) →
+   ∀x,y:Prod3T T1 T2 T3.decidable (x = y).
  #T1; #T2; #T3; #H; #H1; #H2;
  #x; nelim x; #xx1; #xx2; #xx3;
  #y; nelim y; #yy1; #yy2; #yy3;
@@ -317,16 +324,17 @@ nlemma decidable_triple :
 nqed.
 
 nlemma neqtriple_to_neq :
-∀T1,T2,T3.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (∀x,y:T1.f1 x y = false → x ≠ y) →
  (∀x,y:T2.f2 x y = false → x ≠ y) →
  (∀x,y:T3.f3 x y = false → x ≠ y) →
- (∀p1,p2:Prod3T T1 T2 T3. 
-  (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false → p1 ≠ p2)).
- #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
- #p1; nelim p1; #x1; #y1; #z1;
- #p2; nelim p2; #x2; #y2; #z2;
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2;
  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) ?);
@@ -336,14 +344,13 @@ nlemma neqtriple_to_neq :
  ##]
 nqed.
 
-nlemma triple_destruct :
-∀T1,T2,T3.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:T3.decidable (x = y)) →
- (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
-  (triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
-  Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2)).
+nlemma triple_destruct
+ : ∀T1,T2,T3.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   (∀x,y:T3.decidable (x = y)) →
+   ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.(triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
+                                 Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2).
  #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
  nnormalize; #H;
  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
@@ -361,19 +368,20 @@ nlemma triple_destruct :
 nqed.
 
 nlemma neq_to_neqtriple :
-∀T1,T2,T3.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (∀x,y:T1.decidable (x = y)) →
  (∀x,y:T2.decidable (x = y)) →
  (∀x,y:T3.decidable (x = y)) →
  (∀x,y:T1.x ≠ y → f1 x y = false) →
  (∀x,y:T2.x ≠ y → f2 x y = false) →
  (∀x,y:T3.x ≠ y → f3 x y = false) →
- (∀p1,p2:Prod3T T1 T2 T3. 
-  (p1 ≠ p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false)).
- #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
- #p1; nelim p1; #x1; #y1; #z1;
- #p2; nelim p2; #x2; #y2; #z2; #H;
+ (p1 ≠ p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #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 > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
@@ -427,17 +435,18 @@ nlemma quadruple_destruct_4 :
 nqed.
 
 nlemma symmetric_eqquadruple :
-∀T1,T2,T3,T4:Type.
+∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (symmetricT T1 bool f1) →
  (symmetricT T2 bool f2) →
  (symmetricT T3 bool f3) →
  (symmetricT T4 bool f4) →
- (∀p1,p2:Prod4T T1 T2 T3 T4.
-  (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p2 p1)).
- #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
- #p1; nelim p1; #x1; #y1; #z1; #v1;
- #p2; nelim p2; #x2; #y2; #z2; #v2;
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2;
  nnormalize;
  nrewrite > (H x1 x2);
  ncases (f1 x2 x1);
@@ -458,17 +467,18 @@ nlemma symmetric_eqquadruple :
 nqed.
 
 nlemma eq_to_eqquadruple :
-∀T1,T2,T3,T4.
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (∀x,y:T1.x = y → f1 x y = true) →
  (∀x,y:T2.x = y → f2 x y = true) →
  (∀x,y:T3.x = y → f3 x y = true) →
  (∀x,y:T4.x = y → f4 x y = true) →
- (∀p1,p2:Prod4T T1 T2 T3 T4.
-  (p1 = p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true)).
- #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- #p1; nelim p1; #x1; #y1; #z1; #v1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
+ (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #H;
  nnormalize;
  nrewrite > (H1 … (quadruple_destruct_1 … H));
  nnormalize;
@@ -481,30 +491,31 @@ nlemma eq_to_eqquadruple :
 nqed.
 
 nlemma eqquadruple_to_eq :
-∀T1,T2,T3,T4.
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (∀x,y:T1.f1 x y = true → x = y) →
  (∀x,y:T2.f2 x y = true → x = y) →
  (∀x,y:T3.f3 x y = true → x = y) →
  (∀x,y:T4.f4 x y = true → x = y) →
- (∀p1,p2:Prod4T T1 T2 T3 T4.
-  (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true → p1 = p2)).
- #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- #p1; nelim p1; #x1; #y1; #z1; #v1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
+ ##[ ##2: #H5; napply (bool_destruct … H5) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
+ ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
+ ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
  #H5; #H6; #H7; #H8;
  nrewrite > (H5 (refl_eq …));
  nrewrite > (H6 (refl_eq …));
@@ -513,13 +524,13 @@ nlemma eqquadruple_to_eq :
  napply refl_eq.
 nqed.
 
-nlemma decidable_quadruple :
-∀T1,T2,T3,T4.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:T3.decidable (x = y)) →
- (∀x,y:T4.decidable (x = y)) →
- (∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y)).
+nlemma decidable_quadruple
+ : ∀T1,T2,T3,T4.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   (∀x,y:T3.decidable (x = y)) →
+   (∀x,y:T4.decidable (x = y)) →
+   ∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y).
  #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3;
  #x; nelim x; #xx1; #xx2; #xx3; #xx4;
  #y; nelim y; #yy1; #yy2; #yy3; #yy4;
@@ -549,17 +560,18 @@ nlemma decidable_quadruple :
 nqed.
 
 nlemma neqquadruple_to_neq :
-∀T1,T2,T3,T4.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (∀x,y:T1.f1 x y = false → x ≠ y) →
  (∀x,y:T2.f2 x y = false → x ≠ y) →
  (∀x,y:T3.f3 x y = false → x ≠ y) →
  (∀x,y:T4.f4 x y = false → x ≠ y) →
- (∀p1,p2:Prod4T T1 T2 T3 T4. 
-  (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false → p1 ≠ p2)).
- #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- #p1; nelim p1; #x1; #y1; #z1; #v1;
- #p2; nelim p2; #x2; #y2; #z2; #v2;
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2;
  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) ?);
@@ -570,15 +582,15 @@ nlemma neqquadruple_to_neq :
  ##]
 nqed.
 
-nlemma quadruple_destruct :
-∀T1,T2,T3,T4.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:T3.decidable (x = y)) →
- (∀x,y:T4.decidable (x = y)) →
- (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
-  (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
-  Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2)).
+nlemma quadruple_destruct
+ : ∀T1,T2,T3,T4.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   (∀x,y:T3.decidable (x = y)) →
+   (∀x,y:T4.decidable (x = y)) →
+   ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+    (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
+    Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2).
  #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4;
  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
  nnormalize; #H;
@@ -601,8 +613,8 @@ nlemma quadruple_destruct :
 nqed.
 
 nlemma neq_to_neqquadruple :
-∀T1,T2,T3,T4.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (∀x,y:T1.decidable (x = y)) →
  (∀x,y:T2.decidable (x = y)) →
  (∀x,y:T3.decidable (x = y)) →
@@ -611,11 +623,12 @@ nlemma neq_to_neqquadruple :
  (∀x,y:T2.x ≠ y → f2 x y = false) →
  (∀x,y:T3.x ≠ y → f3 x y = false) →
  (∀x,y:T4.x ≠ y → f4 x y = false) →
- (∀p1,p2:Prod4T T1 T2 T3 T4. 
-  (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false)).
- #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
- #p1; nelim p1; #x1; #y1; #z1; #v1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
+ (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #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 > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
@@ -680,18 +693,19 @@ nlemma quintuple_destruct_5 :
 nqed.
 
 nlemma symmetric_eqquintuple :
-∀T1,T2,T3,T4,T5:Type.
+∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (symmetricT T1 bool f1) →
  (symmetricT T2 bool f2) →
  (symmetricT T3 bool f3) →
  (symmetricT T4 bool f4) →
  (symmetricT T5 bool f5) →
- (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
-  (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p2 p1)).
- #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
- #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2;
  nnormalize;
  nrewrite > (H x1 x2);
  ncases (f1 x2 x1);
@@ -717,18 +731,19 @@ nlemma symmetric_eqquintuple :
 nqed.
 
 nlemma eq_to_eqquintuple :
-∀T1,T2,T3,T4,T5.
+∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (∀x,y:T1.x = y → f1 x y = true) →
  (∀x,y:T2.x = y → f2 x y = true) →
  (∀x,y:T3.x = y → f3 x y = true) →
  (∀x,y:T4.x = y → f4 x y = true) →
  (∀x,y:T5.x = y → f5 x y = true) →
- (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
-  (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true)).
- #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
+ (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2; #H;
  nnormalize;
  nrewrite > (H1 … (quintuple_destruct_1 … H));
  nnormalize;
@@ -743,35 +758,36 @@ nlemma eq_to_eqquintuple :
 nqed.
 
 nlemma eqquintuple_to_eq :
-∀T1,T2,T3,T4,T5.
+∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (∀x,y:T1.f1 x y = true → x = y) →
  (∀x,y:T2.f2 x y = true → x = y) →
  (∀x,y:T3.f3 x y = true → x = y) →
  (∀x,y:T4.f4 x y = true → x = y) →
  (∀x,y:T5.f5 x y = true → x = y) →
- (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
-  (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true → p1 = p2)).
- #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
+ ##[ ##2: #H6; napply (bool_destruct … H6) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
+ ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
+ ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
  nletin K3 ≝ (H4 v1 v2);
  ncases (f4 v1 v2) in K3:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
+ ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
  #H6; #H7; #H8; #H9; #H10;
  nrewrite > (H6 (refl_eq …));
  nrewrite > (H7 (refl_eq …));
@@ -781,14 +797,14 @@ nlemma eqquintuple_to_eq :
  napply refl_eq.
 nqed.
 
-nlemma decidable_quintuple :
-∀T1,T2,T3,T4,T5.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:T3.decidable (x = y)) →
- (∀x,y:T4.decidable (x = y)) →
- (∀x,y:T5.decidable (x = y)) →
- (∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y)).
+nlemma decidable_quintuple
+ : ∀T1,T2,T3,T4,T5.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   (∀x,y:T3.decidable (x = y)) →
+   (∀x,y:T4.decidable (x = y)) →
+   (∀x,y:T5.decidable (x = y)) →
+   ∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y).
  #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4;
  #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5;
  #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
@@ -823,18 +839,19 @@ nlemma decidable_quintuple :
 nqed.
 
 nlemma neqquintuple_to_neq :
-∀T1,T2,T3,T4,T5.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (∀x,y:T1.f1 x y = false → x ≠ y) →
  (∀x,y:T2.f2 x y = false → x ≠ y) →
  (∀x,y:T3.f3 x y = false → x ≠ y) →
  (∀x,y:T4.f4 x y = false → x ≠ y) →
  (∀x,y:T5.f5 x y = false → x ≠ y) →
- (∀p1,p2:Prod5T T1 T2 T3 T4 T5. 
-  (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false → p1 ≠ p2)).
- #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2;
  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) ?);
@@ -846,16 +863,16 @@ nlemma neqquintuple_to_neq :
  ##]
 nqed.
 
-nlemma quintuple_destruct :
-∀T1,T2,T3,T4,T5.
- (∀x,y:T1.decidable (x = y)) →
- (∀x,y:T2.decidable (x = y)) →
- (∀x,y:T3.decidable (x = y)) →
- (∀x,y:T4.decidable (x = y)) →
- (∀x,y:T5.decidable (x = y)) →
- (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
-  (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
-  Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2)).
+nlemma quintuple_destruct
+ : ∀T1,T2,T3,T4,T5.
+   (∀x,y:T1.decidable (x = y)) →
+   (∀x,y:T2.decidable (x = y)) →
+   (∀x,y:T3.decidable (x = y)) →
+   (∀x,y:T4.decidable (x = y)) →
+   (∀x,y:T5.decidable (x = y)) →
+   ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+    (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
+    Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2).
  #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5;
  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
  nnormalize; #H;
@@ -882,8 +899,8 @@ nlemma quintuple_destruct :
 nqed.
 
 nlemma neq_to_neqquintuple :
-∀T1,T2,T3,T4,T5.
-∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (∀x,y:T1.decidable (x = y)) →
  (∀x,y:T2.decidable (x = y)) →
  (∀x,y:T3.decidable (x = y)) →
@@ -894,12 +911,14 @@ nlemma neq_to_neqquintuple :
  (∀x,y:T3.x ≠ y → f3 x y = false) →
  (∀x,y:T4.x ≠ y → f4 x y = false) →
  (∀x,y:T5.x ≠ y → f5 x y = false) →
- (∀p1,p2:Prod5T T1 T2 T3 T4 T5. 
-  (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false)).
- #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; 
+ (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2;
+ #f1; #f2; #f3; #f4; #f5;
  #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
- #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
- #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #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 > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq