helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/prod.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ********* *)
  27 (* TUPLE x 2 *)
  28 (* ********* *)
  29
  30 nlemma pair_destruct_1 :
  31 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  32  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
  33  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  34  nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma pair_destruct_2 :
  41 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  42  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
  43  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  44  nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_eqpair :
  51 ∀T1,T2:Type.
  52 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  53  (symmetricT T1 bool f1) →
  54  (symmetricT T2 bool f2) →
  55  (∀p1,p2:ProdT T1 T2.
  56   (eq_pair T1 T2 f1 f2 p1 p2 = eq_pair T1 T2 f1 f2 p1 p2)).
  57  #T1; #T2; #f1; #f2; #H; #H1;
  58  #p1; nelim p1; #x1; #y1;
  59  #p2; nelim p2; #x2; #y2;
  60  nnormalize;
  61  nrewrite > (H x1 x2);
  62  ncases (f1 x2 x1);
  63  nnormalize;
  64  ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
  65  ##| ##2: napply refl_eq
  66  ##]
  67 nqed.
  68
  69 nlemma eq_to_eqpair :
  70 ∀T1,T2.
  71 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  72  (∀x,y:T1.x = y → f1 x y = true) →
  73  (∀x,y:T2.x = y → f2 x y = true) →
  74  (∀p1,p2:ProdT T1 T2.
  75    (p1 = p2 → eq_pair T1 T2 f1 f2 p1 p2 = true)).
  76  #T1; #T2; #f1; #f2; #H1; #H2;
  77  #p1; nelim p1; #x1; #y1;
  78  #p2; nelim p2; #x2; #y2; #H;
  79  nnormalize;
  80  nrewrite > (H1 … (pair_destruct_1 … H));
  81  nnormalize;
  82  nrewrite > (H2 … (pair_destruct_2 … H));
  83  napply refl_eq.
  84 nqed.
  85
  86 nlemma eqpair_to_eq :
  87 ∀T1,T2.
  88 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  89  (∀x,y:T1.f1 x y = true → x = y) →
  90  (∀x,y:T2.f2 x y = true → x = y) →
  91  (∀p1,p2:ProdT T1 T2.
  92   (eq_pair T1 T2 f1 f2 p1 p2 = true → p1 = p2)).
  93  #T1; #T2; #f1; #f2; #H1; #H2;
  94  #p1; nelim p1; #x1; #y1;
  95  #p2; nelim p2; #x2; #y2; #H;
  96  nnormalize in H:(%);
  97  nletin K ≝ (H1 x1 x2);
  98  ncases (f1 x1 x2) in H:(%) K:(%);
  99  nnormalize;
 100  #H3;
 101  ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
 102  #H4;
 103  nrewrite > (H4 (refl_eq …));
 104  nrewrite > (H2 y1 y2 H3);
 105  napply refl_eq.
 106 nqed.
 107
 108 nlemma decidable_pair :
 109 ∀T1,T2.
 110  (∀x,y:T1.decidable (x = y)) →
 111  (∀x,y:T2.decidable (x = y)) →
 112  (∀x,y:ProdT T1 T2.decidable (x = y)).
 113  #T1; #T2; #H; #H1;
 114  #x; nelim x; #xx1; #xx2;
 115  #y; nelim y; #yy1; #yy2;
 116  nnormalize;
 117  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 118  ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 119           nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
 120  ##| ##1: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 121           ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 122                    nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
 123           ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 124                    nrewrite > H2; nrewrite > H3; napply refl_eq
 125           ##]
 126  ##]
 127 nqed.
 128
 129 nlemma neqpair_to_neq :
 130 ∀T1,T2.
 131 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
 132  (∀x,y:T1.f1 x y = false → x ≠ y) →
 133  (∀x,y:T2.f2 x y = false → x ≠ y) →
 134  (∀p1,p2:ProdT T1 T2.
 135   (eq_pair T1 T2 f1 f2 p1 p2 = false → p1 ≠ p2)).
 136  #T1; #T2; #f1; #f2; #H1; #H2;
 137  #p1; nelim p1; #x1; #y1;
 138  #p2; nelim p2; #x2; #y2;
 139  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
 140  nnormalize; #H3;
 141  napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
 142  ##[ ##1: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
 143  ##| ##2: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
 144  ##]
 145 nqed.
 146
 147 nlemma pair_destruct :
 148 ∀T1,T2.
 149  (∀x,y:T1.decidable (x = y)) →
 150  (∀x,y:T2.decidable (x = y)) →
 151  (∀x1,x2:T1.∀y1,y2:T2.
 152   (pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2).
 153  #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
 154  nnormalize; #H;
 155  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 156  ##[ ##2: #H3; napply (or2_intro1 … H3)
 157  ##| ##1: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 158           ##[ ##2: #H4; napply (or2_intro2 … H4)
 159           ##| ##1: #H4; nrewrite > H3 in H:(%);
 160                    nrewrite > H4; #H; nelim (H (refl_eq …))
 161           ##]
 162  ##]
 163 nqed.
 164
 165 nlemma neq_to_neqpair :
 166 ∀T1,T2.
 167 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
 168  (∀x,y:T1.decidable (x = y)) →
 169  (∀x,y:T2.decidable (x = y)) →
 170  (∀x,y:T1.x ≠ y → f1 x y = false) →
 171  (∀x,y:T2.x ≠ y → f2 x y = false) →
 172  (∀p1,p2:ProdT T1 T2.
 173   (p1 ≠ p2 → eq_pair T1 T2 f1 f2 p1 p2 = false)).
 174  #T1; #T2; #f1; #f2; #H1; #H2; #H3; #H4;
 175  #p1; nelim p1; #x1; #y1;
 176  #p2; nelim p2; #x2; #y2; #H;
 177  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
 178  napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
 179  ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
 180  ##| ##1: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
 181  ##]
 182 nqed.
 183
 184 (* ********* *)
 185 (* TUPLE x 3 *)
 186 (* ********* *)
 187
 188 nlemma triple_destruct_1 :
 189 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 190  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
 191  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 192  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
 193  nrewrite < H;
 194  nnormalize;
 195  napply refl_eq.
 196 nqed.
 197
 198 nlemma triple_destruct_2 :
 199 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 200  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
 201  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 202  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
 203  nrewrite < H;
 204  nnormalize;
 205  napply refl_eq.
 206 nqed.
 207
 208 nlemma triple_destruct_3 :
 209 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 210  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
 211  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 212  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
 213  nrewrite < H;
 214  nnormalize;
 215  napply refl_eq.
 216 nqed.
 217
 218 nlemma symmetric_eqtriple :
 219 ∀T1,T2,T3:Type.
 220 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 221  (symmetricT T1 bool f1) →
 222  (symmetricT T2 bool f2) →
 223  (symmetricT T3 bool f3) →
 224  (∀p1,p2:Prod3T T1 T2 T3.
 225   (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = eq_triple T1 T2 T3 f1 f2 f3 p2 p1)).
 226  #T1; #T2; #T3; #f1; #f2; #f3; #H; #H1; #H2;
 227  #p1; nelim p1; #x1; #y1; #z1;
 228  #p2; nelim p2; #x2; #y2; #z2;
 229  nnormalize;
 230  nrewrite > (H x1 x2);
 231  ncases (f1 x2 x1);
 232  nnormalize;
 233  ##[ ##1: nrewrite > (H1 y1 y2);
 234           ncases (f2 y2 y1);
 235           nnormalize;
 236           ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
 237           ##| ##2: napply refl_eq
 238           ##]
 239  ##| ##2: napply refl_eq
 240  ##]
 241 nqed.
 242
 243 nlemma eq_to_eqtriple :
 244 ∀T1,T2,T3.
 245 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 246  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 247  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 248  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 249  (∀p1,p2:Prod3T T1 T2 T3.
 250   (p1 = p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true)).
 251  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
 252  #p1; nelim p1; #x1; #y1; #z1;
 253  #p2; nelim p2; #x2; #y2; #z2; #H;
 254  nnormalize;
 255  nrewrite > (H1 … (triple_destruct_1 … H));
 256  nnormalize;
 257  nrewrite > (H2 … (triple_destruct_2 … H));
 258  nnormalize;
 259  nrewrite > (H3 … (triple_destruct_3 … H));
 260  napply refl_eq.
 261 nqed.
 262
 263 nlemma eqtriple_to_eq :
 264 ∀T1,T2,T3.
 265 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 266  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 267  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 268  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 269  (∀p1,p2:Prod3T T1 T2 T3.
 270   (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true → p1 = p2)).
 271  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
 272  #p1; nelim p1; #x1; #y1; #z1;
 273  #p2; nelim p2; #x2; #y2; #z2; #H;
 274  nnormalize in H:(%);
 275  nletin K ≝ (H1 x1 x2);
 276  ncases (f1 x1 x2) in H:(%) K:(%);
 277  nnormalize;
 278  ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
 279  nletin K1 ≝ (H2 y1 y2);
 280  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 281  nnormalize;
 282  ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
 283  #H4; #H5; #H6;
 284  nrewrite > (H4 (refl_eq …));
 285  nrewrite > (H6 (refl_eq …));
 286  nrewrite > (H3 z1 z2 H5);
 287  napply refl_eq.
 288 nqed.
 289
 290 nlemma decidable_triple :
 291 ∀T1,T2,T3.
 292  (∀x,y:T1.decidable (x = y)) →
 293  (∀x,y:T2.decidable (x = y)) →
 294  (∀x,y:T3.decidable (x = y)) →
 295  (∀x,y:Prod3T T1 T2 T3.decidable (x = y)).
 296  #T1; #T2; #T3; #H; #H1; #H2;
 297  #x; nelim x; #xx1; #xx2; #xx3;
 298  #y; nelim y; #yy1; #yy2; #yy3;
 299  nnormalize;
 300  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 301  ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 302           nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
 303  ##| ##1: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 304           ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 305                    nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
 306           ##| ##1: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
 307                    ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 308                             nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
 309                    ##| ##1: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 310                             nrewrite > H3;
 311                             nrewrite > H4;
 312                             nrewrite > H5;
 313                             napply refl_eq
 314                    ##]
 315           ##]
 316  ##]
 317 nqed.
 318
 319 nlemma neqtriple_to_neq :
 320 ∀T1,T2,T3.
 321 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 322  (∀x,y:T1.f1 x y = false → x ≠ y) →
 323  (∀x,y:T2.f2 x y = false → x ≠ y) →
 324  (∀x,y:T3.f3 x y = false → x ≠ y) →
 325  (∀p1,p2:Prod3T T1 T2 T3.
 326   (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false → p1 ≠ p2)).
 327  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
 328  #p1; nelim p1; #x1; #y1; #z1;
 329  #p2; nelim p2; #x2; #y2; #z2;
 330  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
 331  nnormalize; #H4;
 332  napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
 333  ##[ ##1: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
 334  ##| ##2: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
 335  ##| ##3: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
 336  ##]
 337 nqed.
 338
 339 nlemma triple_destruct :
 340 ∀T1,T2,T3.
 341  (∀x,y:T1.decidable (x = y)) →
 342  (∀x,y:T2.decidable (x = y)) →
 343  (∀x,y:T3.decidable (x = y)) →
 344  (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 345   (triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
 346   Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2)).
 347  #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
 348  nnormalize; #H;
 349  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 350  ##[ ##2: #H4; napply (or3_intro1 … H4)
 351  ##| ##1: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 352           ##[ ##2: #H5; napply (or3_intro2 … H5)
 353           ##| ##1: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
 354                    ##[ ##2: #H6; napply (or3_intro3 … H6)
 355                    ##| ##1: #H6; nrewrite > H4 in H:(%);
 356                             nrewrite > H5;
 357                             nrewrite > H6; #H; nelim (H (refl_eq …))
 358                    ##]
 359           ##]
 360  ##]
 361 nqed.
 362
 363 nlemma neq_to_neqtriple :
 364 ∀T1,T2,T3.
 365 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 366  (∀x,y:T1.decidable (x = y)) →
 367  (∀x,y:T2.decidable (x = y)) →
 368  (∀x,y:T3.decidable (x = y)) →
 369  (∀x,y:T1.x ≠ y → f1 x y = false) →
 370  (∀x,y:T2.x ≠ y → f2 x y = false) →
 371  (∀x,y:T3.x ≠ y → f3 x y = false) →
 372  (∀p1,p2:Prod3T T1 T2 T3.
 373   (p1 ≠ p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false)).
 374  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
 375  #p1; nelim p1; #x1; #y1; #z1;
 376  #p2; nelim p2; #x2; #y2; #z2; #H;
 377  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
 378  napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
 379  ##[ ##1: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
 380  ##| ##2: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
 381  ##| ##3: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
 382  ##]
 383 nqed.
 384
 385 (* ********* *)
 386 (* TUPLE x 4 *)
 387 (* ********* *)
 388
 389 nlemma quadruple_destruct_1 :
 390 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 391  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
 392  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 393  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
 394  nrewrite < H;
 395  nnormalize;
 396  napply refl_eq.
 397 nqed.
 398
 399 nlemma quadruple_destruct_2 :
 400 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 401  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
 402  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 403  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
 404  nrewrite < H;
 405  nnormalize;
 406  napply refl_eq.
 407 nqed.
 408
 409 nlemma quadruple_destruct_3 :
 410 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 411  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
 412  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 413  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
 414  nrewrite < H;
 415  nnormalize;
 416  napply refl_eq.
 417 nqed.
 418
 419 nlemma quadruple_destruct_4 :
 420 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 421  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
 422  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 423  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
 424  nrewrite < H;
 425  nnormalize;
 426  napply refl_eq.
 427 nqed.
 428
 429 nlemma symmetric_eqquadruple :
 430 ∀T1,T2,T3,T4:Type.
 431 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 432  (symmetricT T1 bool f1) →
 433  (symmetricT T2 bool f2) →
 434  (symmetricT T3 bool f3) →
 435  (symmetricT T4 bool f4) →
 436  (∀p1,p2:Prod4T T1 T2 T3 T4.
 437   (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p2 p1)).
 438  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
 439  #p1; nelim p1; #x1; #y1; #z1; #v1;
 440  #p2; nelim p2; #x2; #y2; #z2; #v2;
 441  nnormalize;
 442  nrewrite > (H x1 x2);
 443  ncases (f1 x2 x1);
 444  nnormalize;
 445  ##[ ##1: nrewrite > (H1 y1 y2);
 446           ncases (f2 y2 y1);
 447           nnormalize;
 448           ##[ ##1: nrewrite > (H2 z1 z2);
 449                    ncases (f3 z2 z1);
 450                    nnormalize;
 451                    ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
 452                    ##| ##2: napply refl_eq
 453                    ##]
 454           ##| ##2: napply refl_eq
 455           ##]
 456  ##| ##2: napply refl_eq
 457  ##]
 458 nqed.
 459
 460 nlemma eq_to_eqquadruple :
 461 ∀T1,T2,T3,T4.
 462 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 463  (∀x,y:T1.x = y → f1 x y = true) →
 464  (∀x,y:T2.x = y → f2 x y = true) →
 465  (∀x,y:T3.x = y → f3 x y = true) →
 466  (∀x,y:T4.x = y → f4 x y = true) →
 467  (∀p1,p2:Prod4T T1 T2 T3 T4.
 468   (p1 = p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true)).
 469  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 470  #p1; nelim p1; #x1; #y1; #z1; #v1;
 471  #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
 472  nnormalize;
 473  nrewrite > (H1 … (quadruple_destruct_1 … H));
 474  nnormalize;
 475  nrewrite > (H2 … (quadruple_destruct_2 … H));
 476  nnormalize;
 477  nrewrite > (H3 … (quadruple_destruct_3 … H));
 478  nnormalize;
 479  nrewrite > (H4 … (quadruple_destruct_4 … H));
 480  napply refl_eq.
 481 nqed.
 482
 483 nlemma eqquadruple_to_eq :
 484 ∀T1,T2,T3,T4.
 485 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 486  (∀x,y:T1.f1 x y = true → x = y) →
 487  (∀x,y:T2.f2 x y = true → x = y) →
 488  (∀x,y:T3.f3 x y = true → x = y) →
 489  (∀x,y:T4.f4 x y = true → x = y) →
 490  (∀p1,p2:Prod4T T1 T2 T3 T4.
 491   (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true → p1 = p2)).
 492  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 493  #p1; nelim p1; #x1; #y1; #z1; #v1;
 494  #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
 495  nnormalize in H:(%);
 496  nletin K ≝ (H1 x1 x2);
 497  ncases (f1 x1 x2) in H:(%) K:(%);
 498  nnormalize;
 499  ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
 500  nletin K1 ≝ (H2 y1 y2);
 501  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 502  nnormalize;
 503  ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
 504  nletin K2 ≝ (H3 z1 z2);
 505  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 506  nnormalize;
 507  ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
 508  #H5; #H6; #H7; #H8;
 509  nrewrite > (H5 (refl_eq …));
 510  nrewrite > (H6 (refl_eq …));
 511  nrewrite > (H8 (refl_eq …));
 512  nrewrite > (H4 v1 v2 H7);
 513  napply refl_eq.
 514 nqed.
 515
 516 nlemma decidable_quadruple :
 517 ∀T1,T2,T3,T4.
 518  (∀x,y:T1.decidable (x = y)) →
 519  (∀x,y:T2.decidable (x = y)) →
 520  (∀x,y:T3.decidable (x = y)) →
 521  (∀x,y:T4.decidable (x = y)) →
 522  (∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y)).
 523  #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3;
 524  #x; nelim x; #xx1; #xx2; #xx3; #xx4;
 525  #y; nelim y; #yy1; #yy2; #yy3; #yy4;
 526  nnormalize;
 527  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 528  ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 529           nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
 530  ##| ##1: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 531           ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 532                    nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
 533           ##| ##1: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
 534                    ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 535                             nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
 536                    ##| ##1: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
 537                             ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 538                                      nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
 539                             ##| ##1: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 540                                      nrewrite > H4;
 541                                      nrewrite > H5;
 542                                      nrewrite > H6;
 543                                      nrewrite > H7;
 544                                      napply refl_eq
 545                             ##]
 546                    ##]
 547           ##]
 548  ##]
 549 nqed.
 550
 551 nlemma neqquadruple_to_neq :
 552 ∀T1,T2,T3,T4.
 553 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 554  (∀x,y:T1.f1 x y = false → x ≠ y) →
 555  (∀x,y:T2.f2 x y = false → x ≠ y) →
 556  (∀x,y:T3.f3 x y = false → x ≠ y) →
 557  (∀x,y:T4.f4 x y = false → x ≠ y) →
 558  (∀p1,p2:Prod4T T1 T2 T3 T4.
 559   (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false → p1 ≠ p2)).
 560  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 561  #p1; nelim p1; #x1; #y1; #z1; #v1;
 562  #p2; nelim p2; #x2; #y2; #z2; #v2;
 563  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
 564  nnormalize; #H5;
 565  napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
 566  ##[ ##1: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
 567  ##| ##2: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
 568  ##| ##3: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
 569  ##| ##4: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
 570  ##]
 571 nqed.
 572
 573 nlemma quadruple_destruct :
 574 ∀T1,T2,T3,T4.
 575  (∀x,y:T1.decidable (x = y)) →
 576  (∀x,y:T2.decidable (x = y)) →
 577  (∀x,y:T3.decidable (x = y)) →
 578  (∀x,y:T4.decidable (x = y)) →
 579  (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 580   (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
 581   Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2)).
 582  #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4;
 583  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
 584  nnormalize; #H;
 585  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 586  ##[ ##2: #H5; napply (or4_intro1 … H5)
 587  ##| ##1: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 588           ##[ ##2: #H6; napply (or4_intro2 … H6)
 589           ##| ##1: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
 590                    ##[ ##2: #H7; napply (or4_intro3 … H7)
 591                    ##| ##1: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
 592                             ##[ ##2: #H8; napply (or4_intro4 … H8)
 593                             ##| ##1: #H8; nrewrite > H5 in H:(%);
 594                                      nrewrite > H6;
 595                                      nrewrite > H7;
 596                                      nrewrite > H8; #H; nelim (H (refl_eq …))
 597                             ##]
 598                    ##]
 599           ##]
 600  ##]
 601 nqed.
 602
 603 nlemma neq_to_neqquadruple :
 604 ∀T1,T2,T3,T4.
 605 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 606  (∀x,y:T1.decidable (x = y)) →
 607  (∀x,y:T2.decidable (x = y)) →
 608  (∀x,y:T3.decidable (x = y)) →
 609  (∀x,y:T4.decidable (x = y)) →
 610  (∀x,y:T1.x ≠ y → f1 x y = false) →
 611  (∀x,y:T2.x ≠ y → f2 x y = false) →
 612  (∀x,y:T3.x ≠ y → f3 x y = false) →
 613  (∀x,y:T4.x ≠ y → f4 x y = false) →
 614  (∀p1,p2:Prod4T T1 T2 T3 T4.
 615   (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false)).
 616  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
 617  #p1; nelim p1; #x1; #y1; #z1; #v1;
 618  #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
 619  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
 620  napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
 621  ##[ ##1: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
 622  ##| ##2: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
 623  ##| ##3: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
 624  ##| ##4: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
 625  ##]
 626 nqed.
 627
 628 (* ********* *)
 629 (* TUPLE x 5 *)
 630 (* ********* *)
 631
 632 nlemma quintuple_destruct_1 :
 633 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 634  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
 635  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 636  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
 637  nrewrite < H;
 638  nnormalize;
 639  napply refl_eq.
 640 nqed.
 641
 642 nlemma quintuple_destruct_2 :
 643 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 644  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
 645  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 646  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
 647  nrewrite < H;
 648  nnormalize;
 649  napply refl_eq.
 650 nqed.
 651
 652 nlemma quintuple_destruct_3 :
 653 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 654  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
 655  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 656  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
 657  nrewrite < H;
 658  nnormalize;
 659  napply refl_eq.
 660 nqed.
 661
 662 nlemma quintuple_destruct_4 :
 663 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 664  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
 665  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 666  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
 667  nrewrite < H;
 668  nnormalize;
 669  napply refl_eq.
 670 nqed.
 671
 672 nlemma quintuple_destruct_5 :
 673 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 674  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
 675  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 676  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
 677  nrewrite < H;
 678  nnormalize;
 679  napply refl_eq.
 680 nqed.
 681
 682 nlemma symmetric_eqquintuple :
 683 ∀T1,T2,T3,T4,T5:Type.
 684 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 685  (symmetricT T1 bool f1) →
 686  (symmetricT T2 bool f2) →
 687  (symmetricT T3 bool f3) →
 688  (symmetricT T4 bool f4) →
 689  (symmetricT T5 bool f5) →
 690  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 691   (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)).
 692  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
 693  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 694  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
 695  nnormalize;
 696  nrewrite > (H x1 x2);
 697  ncases (f1 x2 x1);
 698  nnormalize;
 699  ##[ ##1: nrewrite > (H1 y1 y2);
 700           ncases (f2 y2 y1);
 701           nnormalize;
 702           ##[ ##1: nrewrite > (H2 z1 z2);
 703                    ncases (f3 z2 z1);
 704                    nnormalize;
 705                    ##[ ##1: nrewrite > (H3 v1 v2);
 706                             ncases (f4 v2 v1);
 707                             nnormalize;
 708                             ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
 709                             ##| ##2: napply refl_eq
 710                             ##]
 711                    ##| ##2: napply refl_eq
 712                    ##]
 713           ##| ##2: napply refl_eq
 714           ##]
 715  ##| ##2: napply refl_eq
 716  ##]
 717 nqed.
 718
 719 nlemma eq_to_eqquintuple :
 720 ∀T1,T2,T3,T4,T5.
 721 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 722  (∀x,y:T1.x = y → f1 x y = true) →
 723  (∀x,y:T2.x = y → f2 x y = true) →
 724  (∀x,y:T3.x = y → f3 x y = true) →
 725  (∀x,y:T4.x = y → f4 x y = true) →
 726  (∀x,y:T5.x = y → f5 x y = true) →
 727  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 728   (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true)).
 729  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 730  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 731  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
 732  nnormalize;
 733  nrewrite > (H1 … (quintuple_destruct_1 … H));
 734  nnormalize;
 735  nrewrite > (H2 … (quintuple_destruct_2 … H));
 736  nnormalize;
 737  nrewrite > (H3 … (quintuple_destruct_3 … H));
 738  nnormalize;
 739  nrewrite > (H4 … (quintuple_destruct_4 … H));
 740  nnormalize;
 741  nrewrite > (H5 … (quintuple_destruct_5 … H));
 742  napply refl_eq.
 743 nqed.
 744
 745 nlemma eqquintuple_to_eq :
 746 ∀T1,T2,T3,T4,T5.
 747 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 748  (∀x,y:T1.f1 x y = true → x = y) →
 749  (∀x,y:T2.f2 x y = true → x = y) →
 750  (∀x,y:T3.f3 x y = true → x = y) →
 751  (∀x,y:T4.f4 x y = true → x = y) →
 752  (∀x,y:T5.f5 x y = true → x = y) →
 753  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 754   (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true → p1 = p2)).
 755  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 756  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 757  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
 758  nnormalize in H:(%);
 759  nletin K ≝ (H1 x1 x2);
 760  ncases (f1 x1 x2) in H:(%) K:(%);
 761  nnormalize;
 762  ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
 763  nletin K1 ≝ (H2 y1 y2);
 764  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 765  nnormalize;
 766  ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
 767  nletin K2 ≝ (H3 z1 z2);
 768  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 769  nnormalize;
 770  ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
 771  nletin K3 ≝ (H4 v1 v2);
 772  ncases (f4 v1 v2) in K3:(%) ⊢ %;
 773  nnormalize;
 774  ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
 775  #H6; #H7; #H8; #H9; #H10;
 776  nrewrite > (H6 (refl_eq …));
 777  nrewrite > (H7 (refl_eq …));
 778  nrewrite > (H8 (refl_eq …));
 779  nrewrite > (H10 (refl_eq …));
 780  nrewrite > (H5 w1 w2 H9);
 781  napply refl_eq.
 782 nqed.
 783
 784 nlemma decidable_quintuple :
 785 ∀T1,T2,T3,T4,T5.
 786  (∀x,y:T1.decidable (x = y)) →
 787  (∀x,y:T2.decidable (x = y)) →
 788  (∀x,y:T3.decidable (x = y)) →
 789  (∀x,y:T4.decidable (x = y)) →
 790  (∀x,y:T5.decidable (x = y)) →
 791  (∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y)).
 792  #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4;
 793  #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5;
 794  #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
 795  nnormalize;
 796  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 797  ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 798           nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
 799  ##| ##1: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 800           ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 801                    nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
 802           ##| ##1: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
 803                    ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 804                             nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
 805                    ##| ##1: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
 806                             ##[ ##2: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 807                                      nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
 808                             ##| ##1: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
 809                                      ##[ ##2: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 810                                               nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
 811                                      ##| ##1: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 812                                               nrewrite > H5;
 813                                               nrewrite > H6;
 814                                               nrewrite > H7;
 815                                               nrewrite > H8;
 816                                               nrewrite > H9;
 817                                               napply refl_eq
 818                                      ##]
 819                             ##]
 820                    ##]
 821           ##]
 822  ##]
 823 nqed.
 824
 825 nlemma neqquintuple_to_neq :
 826 ∀T1,T2,T3,T4,T5.
 827 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 828  (∀x,y:T1.f1 x y = false → x ≠ y) →
 829  (∀x,y:T2.f2 x y = false → x ≠ y) →
 830  (∀x,y:T3.f3 x y = false → x ≠ y) →
 831  (∀x,y:T4.f4 x y = false → x ≠ y) →
 832  (∀x,y:T5.f5 x y = false → x ≠ y) →
 833  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 834   (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false → p1 ≠ p2)).
 835  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 836  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 837  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
 838  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
 839  nnormalize; #H6;
 840  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) ?);
 841  ##[ ##1: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
 842  ##| ##2: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
 843  ##| ##3: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
 844  ##| ##4: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
 845  ##| ##5: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
 846  ##]
 847 nqed.
 848
 849 nlemma quintuple_destruct :
 850 ∀T1,T2,T3,T4,T5.
 851  (∀x,y:T1.decidable (x = y)) →
 852  (∀x,y:T2.decidable (x = y)) →
 853  (∀x,y:T3.decidable (x = y)) →
 854  (∀x,y:T4.decidable (x = y)) →
 855  (∀x,y:T5.decidable (x = y)) →
 856  (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 857   (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
 858   Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2)).
 859  #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5;
 860  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
 861  nnormalize; #H;
 862  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 863  ##[ ##2: #H6; napply (or5_intro1 … H6)
 864  ##| ##1: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 865           ##[ ##2: #H7; napply (or5_intro2 … H7)
 866           ##| ##1: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
 867                    ##[ ##2: #H8; napply (or5_intro3 … H8)
 868                    ##| ##1: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
 869                             ##[ ##2: #H9; napply (or5_intro4 … H9)
 870                             ##| ##1: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
 871                                      ##[ ##2: #H10; napply (or5_intro5 … H10)
 872                                      ##| ##1: #H10; nrewrite > H6 in H:(%);
 873                                               nrewrite > H7;
 874                                               nrewrite > H8;
 875                                               nrewrite > H9;
 876                                               nrewrite > H10; #H; nelim (H (refl_eq …))
 877                                      ##]
 878                             ##]
 879                    ##]
 880           ##]
 881  ##]
 882 nqed.
 883
 884 nlemma neq_to_neqquintuple :
 885 ∀T1,T2,T3,T4,T5.
 886 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 887  (∀x,y:T1.decidable (x = y)) →
 888  (∀x,y:T2.decidable (x = y)) →
 889  (∀x,y:T3.decidable (x = y)) →
 890  (∀x,y:T4.decidable (x = y)) →
 891  (∀x,y:T5.decidable (x = y)) →
 892  (∀x,y:T1.x ≠ y → f1 x y = false) →
 893  (∀x,y:T2.x ≠ y → f2 x y = false) →
 894  (∀x,y:T3.x ≠ y → f3 x y = false) →
 895  (∀x,y:T4.x ≠ y → f4 x y = false) →
 896  (∀x,y:T5.x ≠ y → f5 x y = false) →
 897  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 898   (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false)).
 899  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5;
 900  #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
 901  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 902  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
 903  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
 904  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) ?);
 905  ##[ ##1: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
 906  ##| ##2: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
 907  ##| ##3: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
 908  ##| ##4: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
 909  ##| ##5: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
 910  ##]
 911 nqed.