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