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