helm/software/matita/contribs/ng_assembly2/common/prod.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/comp.ma".
  24 include "common/prod_base.ma".
  25 include "num/bool_lemmas.ma".
  26
  27 (* ********* *)
  28 (* TUPLE x 2 *)
  29 (* ********* *)
  30
  31 nlemma pair_destruct_1 :
  32 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  33  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
  34  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  35  nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
  36  nrewrite < H;
  37  nnormalize;
  38  napply refl_eq.
  39 nqed.
  40
  41 nlemma pair_destruct_2 :
  42 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  43  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
  44  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  45  nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
  46  nrewrite < H;
  47  nnormalize;
  48  napply refl_eq.
  49 nqed.
  50
  51 nlemma symmetric_eqpair :
  52 ∀T1,T2:Type.
  53 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  54  (symmetricT T1 bool f1) →
  55  (symmetricT T2 bool f2) →
  56  (∀p1,p2:ProdT T1 T2.
  57   (eq_pair T1 T2 f1 f2 p1 p2 = eq_pair T1 T2 f1 f2 p2 p1)).
  58  #T1; #T2; #f1; #f2; #H; #H1;
  59  #p1; nelim p1; #x1; #y1;
  60  #p2; nelim p2; #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.
  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:ProdT T1 T2.
  76    (p1 = p2 → eq_pair T1 T2 f1 f2 p1 p2 = true)).
  77  #T1; #T2; #f1; #f2; #H1; #H2;
  78  #p1; nelim p1; #x1; #y1;
  79  #p2; nelim p2; #x2; #y2; #H;
  80  nnormalize;
  81  nrewrite > (H1 … (pair_destruct_1 … H));
  82  nnormalize;
  83  nrewrite > (H2 … (pair_destruct_2 … H));
  84  napply refl_eq.
  85 nqed.
  86
  87 nlemma eqpair_to_eq :
  88 ∀T1,T2.
  89 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  90  (∀x,y:T1.f1 x y = true → x = y) →
  91  (∀x,y:T2.f2 x y = true → x = y) →
  92  (∀p1,p2:ProdT T1 T2.
  93   (eq_pair T1 T2 f1 f2 p1 p2 = true → p1 = p2)).
  94  #T1; #T2; #f1; #f2; #H1; #H2;
  95  #p1; nelim p1; #x1; #y1;
  96  #p2; nelim p2; #x2; #y2; #H;
  97  nnormalize in H:(%);
  98  nletin K ≝ (H1 x1 x2);
  99  ncases (f1 x1 x2) in H:(%) K:(%);
 100  nnormalize;
 101  #H3;
 102  ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
 103  #H4;
 104  nrewrite > (H4 (refl_eq …));
 105  nrewrite > (H2 y1 y2 H3);
 106  napply refl_eq.
 107 nqed.
 108
 109 nlemma decidable_pair :
 110 ∀T1,T2.
 111  (∀x,y:T1.decidable (x = y)) →
 112  (∀x,y:T2.decidable (x = y)) →
 113  (∀x,y:ProdT T1 T2.decidable (x = y)).
 114  #T1; #T2; #H; #H1;
 115  #x; nelim x; #xx1; #xx2;
 116  #y; nelim y; #yy1; #yy2;
 117  nnormalize;
 118  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 119  ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 120           nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
 121  ##| ##1: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 122           ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 123                    nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
 124           ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 125                    nrewrite > H2; nrewrite > H3; napply refl_eq
 126           ##]
 127  ##]
 128 nqed.
 129
 130 nlemma neqpair_to_neq :
 131 ∀T1,T2.
 132 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
 133  (∀x,y:T1.f1 x y = false → x ≠ y) →
 134  (∀x,y:T2.f2 x y = false → x ≠ y) →
 135  (∀p1,p2:ProdT T1 T2.
 136   (eq_pair T1 T2 f1 f2 p1 p2 = false → p1 ≠ p2)).
 137  #T1; #T2; #f1; #f2; #H1; #H2;
 138  #p1; nelim p1; #x1; #y1;
 139  #p2; nelim p2; #x2; #y2;
 140  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
 141  nnormalize; #H3;
 142  napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
 143  ##[ ##1: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
 144  ##| ##2: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
 145  ##]
 146 nqed.
 147
 148 nlemma pair_destruct :
 149 ∀T1,T2.
 150  (∀x,y:T1.decidable (x = y)) →
 151  (∀x,y:T2.decidable (x = y)) →
 152  (∀x1,x2:T1.∀y1,y2:T2.
 153   (pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2).
 154  #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
 155  nnormalize; #H;
 156  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 157  ##[ ##2: #H3; napply (or2_intro1 … H3)
 158  ##| ##1: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 159           ##[ ##2: #H4; napply (or2_intro2 … H4)
 160           ##| ##1: #H4; nrewrite > H3 in H:(%);
 161                    nrewrite > H4; #H; nelim (H (refl_eq …))
 162           ##]
 163  ##]
 164 nqed.
 165
 166 nlemma neq_to_neqpair :
 167 ∀T1,T2.
 168 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
 169  (∀x,y:T1.decidable (x = y)) →
 170  (∀x,y:T2.decidable (x = y)) →
 171  (∀x,y:T1.x ≠ y → f1 x y = false) →
 172  (∀x,y:T2.x ≠ y → f2 x y = false) →
 173  (∀p1,p2:ProdT T1 T2.
 174   (p1 ≠ p2 → eq_pair T1 T2 f1 f2 p1 p2 = false)).
 175  #T1; #T2; #f1; #f2; #H1; #H2; #H3; #H4;
 176  #p1; nelim p1; #x1; #y1;
 177  #p2; nelim p2; #x2; #y2; #H;
 178  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
 179  napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
 180  ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
 181  ##| ##1: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
 182  ##]
 183 nqed.
 184
 185 nlemma pair_is_comparable :
 186  comparable → comparable → comparable.
 187  #T1; #T2; napply (mk_comparable (ProdT T1 T2));
 188  ##[ napply (pair … (zeroc T1) (zeroc T2))
 189  ##| napply (λP.(forallc T1)
 190              (λe1.(forallc T2)
 191               (λe2.P (pair … e1 e2))))
 192  ##| napply (eq_pair … (eqc T1) (eqc T2))
 193  ##| napply (eqpair_to_eq … (eqc T1) (eqc T2));
 194      ##[ napply (eqc_to_eq T1)
 195      ##| napply (eqc_to_eq T2)
 196      ##]
 197  ##| napply (eq_to_eqpair … (eqc T1) (eqc T2));
 198      ##[ napply (eq_to_eqc T1)
 199      ##| napply (eq_to_eqc T2)
 200      ##]
 201  ##| napply (neqpair_to_neq … (eqc T1) (eqc T2));
 202      ##[ napply (neqc_to_neq T1)
 203      ##| napply (neqc_to_neq T2)
 204      ##]
 205  ##| napply (neq_to_neqpair … (eqc T1) (eqc T2));
 206      ##[ napply (decidable_c T1)
 207      ##| napply (decidable_c T2)
 208      ##| napply (neq_to_neqc T1)
 209      ##| napply (neq_to_neqc T2)
 210      ##]
 211  ##| napply decidable_pair;
 212      ##[ napply (decidable_c T1)
 213      ##| napply (decidable_c T2)
 214      ##]
 215  ##| napply symmetric_eqpair;
 216      ##[ napply (symmetric_eqc T1)
 217      ##| napply (symmetric_eqc T2)
 218      ##]
 219  ##]
 220 nqed.
 221
 222 unification hint 0 ≔ S1: comparable, S2: comparable;
 223          T1 ≟ (carr S1), T2 ≟ (carr S2),
 224          X ≟ (pair_is_comparable S1 S2)
 225  (*********************************************) ⊢
 226          carr X ≡ ProdT T1 T2.
 227
 228 (* ********* *)
 229 (* TUPLE x 3 *)
 230 (* ********* *)
 231
 232 nlemma triple_destruct_1 :
 233 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 234  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
 235  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 236  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
 237  nrewrite < H;
 238  nnormalize;
 239  napply refl_eq.
 240 nqed.
 241
 242 nlemma triple_destruct_2 :
 243 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 244  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
 245  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 246  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
 247  nrewrite < H;
 248  nnormalize;
 249  napply refl_eq.
 250 nqed.
 251
 252 nlemma triple_destruct_3 :
 253 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 254  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
 255  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 256  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
 257  nrewrite < H;
 258  nnormalize;
 259  napply refl_eq.
 260 nqed.
 261
 262 nlemma symmetric_eqtriple :
 263 ∀T1,T2,T3:Type.
 264 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 265  (symmetricT T1 bool f1) →
 266  (symmetricT T2 bool f2) →
 267  (symmetricT T3 bool f3) →
 268  (∀p1,p2:Prod3T T1 T2 T3.
 269   (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = eq_triple T1 T2 T3 f1 f2 f3 p2 p1)).
 270  #T1; #T2; #T3; #f1; #f2; #f3; #H; #H1; #H2;
 271  #p1; nelim p1; #x1; #y1; #z1;
 272  #p2; nelim p2; #x2; #y2; #z2;
 273  nnormalize;
 274  nrewrite > (H x1 x2);
 275  ncases (f1 x2 x1);
 276  nnormalize;
 277  ##[ ##1: nrewrite > (H1 y1 y2);
 278           ncases (f2 y2 y1);
 279           nnormalize;
 280           ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
 281           ##| ##2: napply refl_eq
 282           ##]
 283  ##| ##2: napply refl_eq
 284  ##]
 285 nqed.
 286
 287 nlemma eq_to_eqtriple :
 288 ∀T1,T2,T3.
 289 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 290  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 291  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 292  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 293  (∀p1,p2:Prod3T T1 T2 T3.
 294   (p1 = p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true)).
 295  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
 296  #p1; nelim p1; #x1; #y1; #z1;
 297  #p2; nelim p2; #x2; #y2; #z2; #H;
 298  nnormalize;
 299  nrewrite > (H1 … (triple_destruct_1 … H));
 300  nnormalize;
 301  nrewrite > (H2 … (triple_destruct_2 … H));
 302  nnormalize;
 303  nrewrite > (H3 … (triple_destruct_3 … H));
 304  napply refl_eq.
 305 nqed.
 306
 307 nlemma eqtriple_to_eq :
 308 ∀T1,T2,T3.
 309 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 310  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 311  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 312  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 313  (∀p1,p2:Prod3T T1 T2 T3.
 314   (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true → p1 = p2)).
 315  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
 316  #p1; nelim p1; #x1; #y1; #z1;
 317  #p2; nelim p2; #x2; #y2; #z2; #H;
 318  nnormalize in H:(%);
 319  nletin K ≝ (H1 x1 x2);
 320  ncases (f1 x1 x2) in H:(%) K:(%);
 321  nnormalize;
 322  ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
 323  nletin K1 ≝ (H2 y1 y2);
 324  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 325  nnormalize;
 326  ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
 327  #H4; #H5; #H6;
 328  nrewrite > (H4 (refl_eq …));
 329  nrewrite > (H6 (refl_eq …));
 330  nrewrite > (H3 z1 z2 H5);
 331  napply refl_eq.
 332 nqed.
 333
 334 nlemma decidable_triple :
 335 ∀T1,T2,T3.
 336  (∀x,y:T1.decidable (x = y)) →
 337  (∀x,y:T2.decidable (x = y)) →
 338  (∀x,y:T3.decidable (x = y)) →
 339  (∀x,y:Prod3T T1 T2 T3.decidable (x = y)).
 340  #T1; #T2; #T3; #H; #H1; #H2;
 341  #x; nelim x; #xx1; #xx2; #xx3;
 342  #y; nelim y; #yy1; #yy2; #yy3;
 343  nnormalize;
 344  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 345  ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 346           nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
 347  ##| ##1: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 348           ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 349                    nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
 350           ##| ##1: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
 351                    ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 352                             nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
 353                    ##| ##1: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 354                             nrewrite > H3;
 355                             nrewrite > H4;
 356                             nrewrite > H5;
 357                             napply refl_eq
 358                    ##]
 359           ##]
 360  ##]
 361 nqed.
 362
 363 nlemma neqtriple_to_neq :
 364 ∀T1,T2,T3.
 365 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 366  (∀x,y:T1.f1 x y = false → x ≠ y) →
 367  (∀x,y:T2.f2 x y = false → x ≠ y) →
 368  (∀x,y:T3.f3 x y = false → x ≠ y) →
 369  (∀p1,p2:Prod3T T1 T2 T3.
 370   (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false → p1 ≠ p2)).
 371  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
 372  #p1; nelim p1; #x1; #y1; #z1;
 373  #p2; nelim p2; #x2; #y2; #z2;
 374  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
 375  nnormalize; #H4;
 376  napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
 377  ##[ ##1: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
 378  ##| ##2: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
 379  ##| ##3: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
 380  ##]
 381 nqed.
 382
 383 nlemma triple_destruct :
 384 ∀T1,T2,T3.
 385  (∀x,y:T1.decidable (x = y)) →
 386  (∀x,y:T2.decidable (x = y)) →
 387  (∀x,y:T3.decidable (x = y)) →
 388  (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 389   (triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
 390   Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2)).
 391  #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
 392  nnormalize; #H;
 393  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 394  ##[ ##2: #H4; napply (or3_intro1 … H4)
 395  ##| ##1: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 396           ##[ ##2: #H5; napply (or3_intro2 … H5)
 397           ##| ##1: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
 398                    ##[ ##2: #H6; napply (or3_intro3 … H6)
 399                    ##| ##1: #H6; nrewrite > H4 in H:(%);
 400                             nrewrite > H5;
 401                             nrewrite > H6; #H; nelim (H (refl_eq …))
 402                    ##]
 403           ##]
 404  ##]
 405 nqed.
 406
 407 nlemma neq_to_neqtriple :
 408 ∀T1,T2,T3.
 409 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 410  (∀x,y:T1.decidable (x = y)) →
 411  (∀x,y:T2.decidable (x = y)) →
 412  (∀x,y:T3.decidable (x = y)) →
 413  (∀x,y:T1.x ≠ y → f1 x y = false) →
 414  (∀x,y:T2.x ≠ y → f2 x y = false) →
 415  (∀x,y:T3.x ≠ y → f3 x y = false) →
 416  (∀p1,p2:Prod3T T1 T2 T3.
 417   (p1 ≠ p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false)).
 418  #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
 419  #p1; nelim p1; #x1; #y1; #z1;
 420  #p2; nelim p2; #x2; #y2; #z2; #H;
 421  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
 422  napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
 423  ##[ ##1: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
 424  ##| ##2: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
 425  ##| ##3: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
 426  ##]
 427 nqed.
 428
 429 nlemma triple_is_comparable :
 430  comparable → comparable → comparable → comparable.
 431  #T1; #T2; #T3; napply (mk_comparable (Prod3T T1 T2 T3));
 432  ##[ napply (triple … (zeroc T1) (zeroc T2) (zeroc T3))
 433  ##| napply (λP.(forallc T1)
 434              (λe1.(forallc T2)
 435               (λe2.(forallc T3)
 436                (λe3.P (triple … e1 e2 e3)))))
 437  ##| napply (eq_triple … (eqc T1) (eqc T2) (eqc T3))
 438  ##| napply (eqtriple_to_eq … (eqc T1) (eqc T2) (eqc T3));
 439      ##[ napply (eqc_to_eq T1)
 440      ##| napply (eqc_to_eq T2)
 441      ##| napply (eqc_to_eq T3)
 442      ##]
 443  ##| napply (eq_to_eqtriple … (eqc T1) (eqc T2) (eqc T3));
 444      ##[ napply (eq_to_eqc T1)
 445      ##| napply (eq_to_eqc T2)
 446      ##| napply (eq_to_eqc T3)
 447      ##]
 448  ##| napply (neqtriple_to_neq … (eqc T1) (eqc T2) (eqc T3));
 449      ##[ napply (neqc_to_neq T1)
 450      ##| napply (neqc_to_neq T2)
 451      ##| napply (neqc_to_neq T3)
 452      ##]
 453  ##| napply (neq_to_neqtriple … (eqc T1) (eqc T2) (eqc T3));
 454      ##[ napply (decidable_c T1)
 455      ##| napply (decidable_c T2)
 456      ##| napply (decidable_c T3)
 457      ##| napply (neq_to_neqc T1)
 458      ##| napply (neq_to_neqc T2)
 459      ##| napply (neq_to_neqc T3)
 460      ##]
 461  ##| napply decidable_triple;
 462      ##[ napply (decidable_c T1)
 463      ##| napply (decidable_c T2)
 464      ##| napply (decidable_c T3)
 465      ##]
 466  ##| napply symmetric_eqtriple;
 467      ##[ napply (symmetric_eqc T1)
 468      ##| napply (symmetric_eqc T2)
 469      ##| napply (symmetric_eqc T3)
 470      ##]
 471  ##]
 472 nqed.
 473
 474 unification hint 0 ≔ S1: comparable, S2: comparable, S3: comparable;
 475          T1 ≟ (carr S1), T2 ≟ (carr S2), T3 ≟ (carr S3),
 476          X ≟ (triple_is_comparable S1 S2 S3)
 477  (*********************************************) ⊢
 478          carr X ≡ Prod3T T1 T2 T3.
 479
 480 (* ********* *)
 481 (* TUPLE x 4 *)
 482 (* ********* *)
 483
 484 nlemma quadruple_destruct_1 :
 485 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 486  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
 487  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 488  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
 489  nrewrite < H;
 490  nnormalize;
 491  napply refl_eq.
 492 nqed.
 493
 494 nlemma quadruple_destruct_2 :
 495 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 496  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
 497  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 498  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
 499  nrewrite < H;
 500  nnormalize;
 501  napply refl_eq.
 502 nqed.
 503
 504 nlemma quadruple_destruct_3 :
 505 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 506  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
 507  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 508  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
 509  nrewrite < H;
 510  nnormalize;
 511  napply refl_eq.
 512 nqed.
 513
 514 nlemma quadruple_destruct_4 :
 515 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 516  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
 517  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 518  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
 519  nrewrite < H;
 520  nnormalize;
 521  napply refl_eq.
 522 nqed.
 523
 524 nlemma symmetric_eqquadruple :
 525 ∀T1,T2,T3,T4:Type.
 526 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 527  (symmetricT T1 bool f1) →
 528  (symmetricT T2 bool f2) →
 529  (symmetricT T3 bool f3) →
 530  (symmetricT T4 bool f4) →
 531  (∀p1,p2:Prod4T T1 T2 T3 T4.
 532   (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p2 p1)).
 533  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
 534  #p1; nelim p1; #x1; #y1; #z1; #v1;
 535  #p2; nelim p2; #x2; #y2; #z2; #v2;
 536  nnormalize;
 537  nrewrite > (H x1 x2);
 538  ncases (f1 x2 x1);
 539  nnormalize;
 540  ##[ ##1: nrewrite > (H1 y1 y2);
 541           ncases (f2 y2 y1);
 542           nnormalize;
 543           ##[ ##1: nrewrite > (H2 z1 z2);
 544                    ncases (f3 z2 z1);
 545                    nnormalize;
 546                    ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
 547                    ##| ##2: napply refl_eq
 548                    ##]
 549           ##| ##2: napply refl_eq
 550           ##]
 551  ##| ##2: napply refl_eq
 552  ##]
 553 nqed.
 554
 555 nlemma eq_to_eqquadruple :
 556 ∀T1,T2,T3,T4.
 557 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 558  (∀x,y:T1.x = y → f1 x y = true) →
 559  (∀x,y:T2.x = y → f2 x y = true) →
 560  (∀x,y:T3.x = y → f3 x y = true) →
 561  (∀x,y:T4.x = y → f4 x y = true) →
 562  (∀p1,p2:Prod4T T1 T2 T3 T4.
 563   (p1 = p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true)).
 564  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 565  #p1; nelim p1; #x1; #y1; #z1; #v1;
 566  #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
 567  nnormalize;
 568  nrewrite > (H1 … (quadruple_destruct_1 … H));
 569  nnormalize;
 570  nrewrite > (H2 … (quadruple_destruct_2 … H));
 571  nnormalize;
 572  nrewrite > (H3 … (quadruple_destruct_3 … H));
 573  nnormalize;
 574  nrewrite > (H4 … (quadruple_destruct_4 … H));
 575  napply refl_eq.
 576 nqed.
 577
 578 nlemma eqquadruple_to_eq :
 579 ∀T1,T2,T3,T4.
 580 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 581  (∀x,y:T1.f1 x y = true → x = y) →
 582  (∀x,y:T2.f2 x y = true → x = y) →
 583  (∀x,y:T3.f3 x y = true → x = y) →
 584  (∀x,y:T4.f4 x y = true → x = y) →
 585  (∀p1,p2:Prod4T T1 T2 T3 T4.
 586   (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true → p1 = p2)).
 587  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 588  #p1; nelim p1; #x1; #y1; #z1; #v1;
 589  #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
 590  nnormalize in H:(%);
 591  nletin K ≝ (H1 x1 x2);
 592  ncases (f1 x1 x2) in H:(%) K:(%);
 593  nnormalize;
 594  ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
 595  nletin K1 ≝ (H2 y1 y2);
 596  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 597  nnormalize;
 598  ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
 599  nletin K2 ≝ (H3 z1 z2);
 600  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 601  nnormalize;
 602  ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
 603  #H5; #H6; #H7; #H8;
 604  nrewrite > (H5 (refl_eq …));
 605  nrewrite > (H6 (refl_eq …));
 606  nrewrite > (H8 (refl_eq …));
 607  nrewrite > (H4 v1 v2 H7);
 608  napply refl_eq.
 609 nqed.
 610
 611 nlemma decidable_quadruple :
 612 ∀T1,T2,T3,T4.
 613  (∀x,y:T1.decidable (x = y)) →
 614  (∀x,y:T2.decidable (x = y)) →
 615  (∀x,y:T3.decidable (x = y)) →
 616  (∀x,y:T4.decidable (x = y)) →
 617  (∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y)).
 618  #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3;
 619  #x; nelim x; #xx1; #xx2; #xx3; #xx4;
 620  #y; nelim y; #yy1; #yy2; #yy3; #yy4;
 621  nnormalize;
 622  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 623  ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 624           nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
 625  ##| ##1: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 626           ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 627                    nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
 628           ##| ##1: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
 629                    ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 630                             nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
 631                    ##| ##1: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
 632                             ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 633                                      nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
 634                             ##| ##1: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 635                                      nrewrite > H4;
 636                                      nrewrite > H5;
 637                                      nrewrite > H6;
 638                                      nrewrite > H7;
 639                                      napply refl_eq
 640                             ##]
 641                    ##]
 642           ##]
 643  ##]
 644 nqed.
 645
 646 nlemma neqquadruple_to_neq :
 647 ∀T1,T2,T3,T4.
 648 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 649  (∀x,y:T1.f1 x y = false → x ≠ y) →
 650  (∀x,y:T2.f2 x y = false → x ≠ y) →
 651  (∀x,y:T3.f3 x y = false → x ≠ y) →
 652  (∀x,y:T4.f4 x y = false → x ≠ y) →
 653  (∀p1,p2:Prod4T T1 T2 T3 T4.
 654   (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false → p1 ≠ p2)).
 655  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 656  #p1; nelim p1; #x1; #y1; #z1; #v1;
 657  #p2; nelim p2; #x2; #y2; #z2; #v2;
 658  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
 659  nnormalize; #H5;
 660  napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
 661  ##[ ##1: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
 662  ##| ##2: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
 663  ##| ##3: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
 664  ##| ##4: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
 665  ##]
 666 nqed.
 667
 668 nlemma quadruple_destruct :
 669 ∀T1,T2,T3,T4.
 670  (∀x,y:T1.decidable (x = y)) →
 671  (∀x,y:T2.decidable (x = y)) →
 672  (∀x,y:T3.decidable (x = y)) →
 673  (∀x,y:T4.decidable (x = y)) →
 674  (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 675   (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
 676   Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2)).
 677  #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4;
 678  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
 679  nnormalize; #H;
 680  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
 681  ##[ ##2: #H5; napply (or4_intro1 … H5)
 682  ##| ##1: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
 683           ##[ ##2: #H6; napply (or4_intro2 … H6)
 684           ##| ##1: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
 685                    ##[ ##2: #H7; napply (or4_intro3 … H7)
 686                    ##| ##1: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
 687                             ##[ ##2: #H8; napply (or4_intro4 … H8)
 688                             ##| ##1: #H8; nrewrite > H5 in H:(%);
 689                                      nrewrite > H6;
 690                                      nrewrite > H7;
 691                                      nrewrite > H8; #H; nelim (H (refl_eq …))
 692                             ##]
 693                    ##]
 694           ##]
 695  ##]
 696 nqed.
 697
 698 nlemma neq_to_neqquadruple :
 699 ∀T1,T2,T3,T4.
 700 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 701  (∀x,y:T1.decidable (x = y)) →
 702  (∀x,y:T2.decidable (x = y)) →
 703  (∀x,y:T3.decidable (x = y)) →
 704  (∀x,y:T4.decidable (x = y)) →
 705  (∀x,y:T1.x ≠ y → f1 x y = false) →
 706  (∀x,y:T2.x ≠ y → f2 x y = false) →
 707  (∀x,y:T3.x ≠ y → f3 x y = false) →
 708  (∀x,y:T4.x ≠ y → f4 x y = false) →
 709  (∀p1,p2:Prod4T T1 T2 T3 T4.
 710   (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false)).
 711  #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
 712  #p1; nelim p1; #x1; #y1; #z1; #v1;
 713  #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
 714  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
 715  napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
 716  ##[ ##1: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
 717  ##| ##2: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
 718  ##| ##3: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
 719  ##| ##4: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
 720  ##]
 721 nqed.
 722
 723 nlemma quadruple_is_comparable :
 724  comparable → comparable → comparable → comparable → comparable.
 725  #T1; #T2; #T3; #T4; napply (mk_comparable (Prod4T T1 T2 T3 T4));
 726  ##[ napply (quadruple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4))
 727  ##| napply (λP.(forallc T1)
 728              (λe1.(forallc T2)
 729               (λe2.(forallc T3)
 730                (λe3.(forallc T4)
 731                 (λe4.P (quadruple … e1 e2 e3 e4))))))
 732  ##| napply (eq_quadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4))
 733  ##| napply (eqquadruple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
 734      ##[ napply (eqc_to_eq T1)
 735      ##| napply (eqc_to_eq T2)
 736      ##| napply (eqc_to_eq T3)
 737      ##| napply (eqc_to_eq T4)
 738      ##]
 739  ##| napply (eq_to_eqquadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
 740      ##[ napply (eq_to_eqc T1)
 741      ##| napply (eq_to_eqc T2)
 742      ##| napply (eq_to_eqc T3)
 743      ##| napply (eq_to_eqc T4)
 744      ##]
 745  ##| napply (neqquadruple_to_neq … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
 746      ##[ napply (neqc_to_neq T1)
 747      ##| napply (neqc_to_neq T2)
 748      ##| napply (neqc_to_neq T3)
 749      ##| napply (neqc_to_neq T4)
 750      ##]
 751  ##| napply (neq_to_neqquadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
 752      ##[ napply (decidable_c T1)
 753      ##| napply (decidable_c T2)
 754      ##| napply (decidable_c T3)
 755      ##| napply (decidable_c T4)
 756      ##| napply (neq_to_neqc T1)
 757      ##| napply (neq_to_neqc T2)
 758      ##| napply (neq_to_neqc T3)
 759      ##| napply (neq_to_neqc T4)
 760      ##]
 761  ##| napply decidable_quadruple;
 762      ##[ napply (decidable_c T1)
 763      ##| napply (decidable_c T2)
 764      ##| napply (decidable_c T3)
 765      ##| napply (decidable_c T4)
 766      ##]
 767  ##| napply symmetric_eqquadruple;
 768      ##[ napply (symmetric_eqc T1)
 769      ##| napply (symmetric_eqc T2)
 770      ##| napply (symmetric_eqc T3)
 771      ##| napply (symmetric_eqc T4)
 772      ##]
 773  ##]
 774 nqed.
 775
 776 unification hint 0 ≔ S1: comparable, S2: comparable, S3: comparable, S4: comparable;
 777          T1 ≟ (carr S1), T2 ≟ (carr S2), T3 ≟ (carr S3), T4 ≟ (carr S4),
 778          X ≟ (quadruple_is_comparable S1 S2 S3 S4)
 779  (*********************************************) ⊢
 780          carr X ≡ Prod4T T1 T2 T3 T4.
 781
 782 (* ********* *)
 783 (* TUPLE x 5 *)
 784 (* ********* *)
 785
 786 nlemma quintuple_destruct_1 :
 787 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 788  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
 789  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 790  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
 791  nrewrite < H;
 792  nnormalize;
 793  napply refl_eq.
 794 nqed.
 795
 796 nlemma quintuple_destruct_2 :
 797 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 798  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
 799  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 800  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
 801  nrewrite < H;
 802  nnormalize;
 803  napply refl_eq.
 804 nqed.
 805
 806 nlemma quintuple_destruct_3 :
 807 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 808  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
 809  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 810  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
 811  nrewrite < H;
 812  nnormalize;
 813  napply refl_eq.
 814 nqed.
 815
 816 nlemma quintuple_destruct_4 :
 817 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 818  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
 819  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 820  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
 821  nrewrite < H;
 822  nnormalize;
 823  napply refl_eq.
 824 nqed.
 825
 826 nlemma quintuple_destruct_5 :
 827 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 828  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
 829  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 830  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
 831  nrewrite < H;
 832  nnormalize;
 833  napply refl_eq.
 834 nqed.
 835
 836 nlemma symmetric_eqquintuple :
 837 ∀T1,T2,T3,T4,T5:Type.
 838 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 839  (symmetricT T1 bool f1) →
 840  (symmetricT T2 bool f2) →
 841  (symmetricT T3 bool f3) →
 842  (symmetricT T4 bool f4) →
 843  (symmetricT T5 bool f5) →
 844  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 845   (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)).
 846  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
 847  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 848  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
 849  nnormalize;
 850  nrewrite > (H x1 x2);
 851  ncases (f1 x2 x1);
 852  nnormalize;
 853  ##[ ##1: nrewrite > (H1 y1 y2);
 854           ncases (f2 y2 y1);
 855           nnormalize;
 856           ##[ ##1: nrewrite > (H2 z1 z2);
 857                    ncases (f3 z2 z1);
 858                    nnormalize;
 859                    ##[ ##1: nrewrite > (H3 v1 v2);
 860                             ncases (f4 v2 v1);
 861                             nnormalize;
 862                             ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
 863                             ##| ##2: napply refl_eq
 864                             ##]
 865                    ##| ##2: napply refl_eq
 866                    ##]
 867           ##| ##2: napply refl_eq
 868           ##]
 869  ##| ##2: napply refl_eq
 870  ##]
 871 nqed.
 872
 873 nlemma eq_to_eqquintuple :
 874 ∀T1,T2,T3,T4,T5.
 875 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 876  (∀x,y:T1.x = y → f1 x y = true) →
 877  (∀x,y:T2.x = y → f2 x y = true) →
 878  (∀x,y:T3.x = y → f3 x y = true) →
 879  (∀x,y:T4.x = y → f4 x y = true) →
 880  (∀x,y:T5.x = y → f5 x y = true) →
 881  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 882   (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true)).
 883  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 884  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 885  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
 886  nnormalize;
 887  nrewrite > (H1 … (quintuple_destruct_1 … H));
 888  nnormalize;
 889  nrewrite > (H2 … (quintuple_destruct_2 … H));
 890  nnormalize;
 891  nrewrite > (H3 … (quintuple_destruct_3 … H));
 892  nnormalize;
 893  nrewrite > (H4 … (quintuple_destruct_4 … H));
 894  nnormalize;
 895  nrewrite > (H5 … (quintuple_destruct_5 … H));
 896  napply refl_eq.
 897 nqed.
 898
 899 nlemma eqquintuple_to_eq :
 900 ∀T1,T2,T3,T4,T5.
 901 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 902  (∀x,y:T1.f1 x y = true → x = y) →
 903  (∀x,y:T2.f2 x y = true → x = y) →
 904  (∀x,y:T3.f3 x y = true → x = y) →
 905  (∀x,y:T4.f4 x y = true → x = y) →
 906  (∀x,y:T5.f5 x y = true → x = y) →
 907  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 908   (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true → p1 = p2)).
 909  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 910  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 911  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
 912  nnormalize in H:(%);
 913  nletin K ≝ (H1 x1 x2);
 914  ncases (f1 x1 x2) in H:(%) K:(%);
 915  nnormalize;
 916  ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
 917  nletin K1 ≝ (H2 y1 y2);
 918  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 919  nnormalize;
 920  ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
 921  nletin K2 ≝ (H3 z1 z2);
 922  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 923  nnormalize;
 924  ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
 925  nletin K3 ≝ (H4 v1 v2);
 926  ncases (f4 v1 v2) in K3:(%) ⊢ %;
 927  nnormalize;
 928  ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
 929  #H6; #H7; #H8; #H9; #H10;
 930  nrewrite > (H6 (refl_eq …));
 931  nrewrite > (H7 (refl_eq …));
 932  nrewrite > (H8 (refl_eq …));
 933  nrewrite > (H10 (refl_eq …));
 934  nrewrite > (H5 w1 w2 H9);
 935  napply refl_eq.
 936 nqed.
 937
 938 nlemma decidable_quintuple :
 939 ∀T1,T2,T3,T4,T5.
 940  (∀x,y:T1.decidable (x = y)) →
 941  (∀x,y:T2.decidable (x = y)) →
 942  (∀x,y:T3.decidable (x = y)) →
 943  (∀x,y:T4.decidable (x = y)) →
 944  (∀x,y:T5.decidable (x = y)) →
 945  (∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y)).
 946  #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4;
 947  #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5;
 948  #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
 949  nnormalize;
 950  napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
 951  ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 952           nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
 953  ##| ##1: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
 954           ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 955                    nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
 956           ##| ##1: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
 957                    ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 958                             nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
 959                    ##| ##1: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
 960                             ##[ ##2: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 961                                      nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
 962                             ##| ##1: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
 963                                      ##[ ##2: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 964                                               nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
 965                                      ##| ##1: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 966                                               nrewrite > H5;
 967                                               nrewrite > H6;
 968                                               nrewrite > H7;
 969                                               nrewrite > H8;
 970                                               nrewrite > H9;
 971                                               napply refl_eq
 972                                      ##]
 973                             ##]
 974                    ##]
 975           ##]
 976  ##]
 977 nqed.
 978
 979 nlemma neqquintuple_to_neq :
 980 ∀T1,T2,T3,T4,T5.
 981 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 982  (∀x,y:T1.f1 x y = false → x ≠ y) →
 983  (∀x,y:T2.f2 x y = false → x ≠ y) →
 984  (∀x,y:T3.f3 x y = false → x ≠ y) →
 985  (∀x,y:T4.f4 x y = false → x ≠ y) →
 986  (∀x,y:T5.f5 x y = false → x ≠ y) →
 987  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 988   (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false → p1 ≠ p2)).
 989  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 990  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
 991  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
 992  nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
 993  nnormalize; #H6;
 994  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) ?);
 995  ##[ ##1: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
 996  ##| ##2: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
 997  ##| ##3: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
 998  ##| ##4: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
 999  ##| ##5: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
1000  ##]
1001 nqed.
1002
1003 nlemma quintuple_destruct :
1004 ∀T1,T2,T3,T4,T5.
1005  (∀x,y:T1.decidable (x = y)) →
1006  (∀x,y:T2.decidable (x = y)) →
1007  (∀x,y:T3.decidable (x = y)) →
1008  (∀x,y:T4.decidable (x = y)) →
1009  (∀x,y:T5.decidable (x = y)) →
1010  (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
1011   (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
1012   Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2)).
1013  #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5;
1014  #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
1015  nnormalize; #H;
1016  napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
1017  ##[ ##2: #H6; napply (or5_intro1 … H6)
1018  ##| ##1: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
1019           ##[ ##2: #H7; napply (or5_intro2 … H7)
1020           ##| ##1: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
1021                    ##[ ##2: #H8; napply (or5_intro3 … H8)
1022                    ##| ##1: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
1023                             ##[ ##2: #H9; napply (or5_intro4 … H9)
1024                             ##| ##1: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
1025                                      ##[ ##2: #H10; napply (or5_intro5 … H10)
1026                                      ##| ##1: #H10; nrewrite > H6 in H:(%);
1027                                               nrewrite > H7;
1028                                               nrewrite > H8;
1029                                               nrewrite > H9;
1030                                               nrewrite > H10; #H; nelim (H (refl_eq …))
1031                                      ##]
1032                             ##]
1033                    ##]
1034           ##]
1035  ##]
1036 nqed.
1037
1038 nlemma neq_to_neqquintuple :
1039 ∀T1,T2,T3,T4,T5.
1040 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
1041  (∀x,y:T1.decidable (x = y)) →
1042  (∀x,y:T2.decidable (x = y)) →
1043  (∀x,y:T3.decidable (x = y)) →
1044  (∀x,y:T4.decidable (x = y)) →
1045  (∀x,y:T5.decidable (x = y)) →
1046  (∀x,y:T1.x ≠ y → f1 x y = false) →
1047  (∀x,y:T2.x ≠ y → f2 x y = false) →
1048  (∀x,y:T3.x ≠ y → f3 x y = false) →
1049  (∀x,y:T4.x ≠ y → f4 x y = false) →
1050  (∀x,y:T5.x ≠ y → f5 x y = false) →
1051  (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
1052   (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false)).
1053  #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5;
1054  #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
1055  #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
1056  #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
1057  nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
1058  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) ?);
1059  ##[ ##1: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
1060  ##| ##2: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
1061  ##| ##3: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
1062  ##| ##4: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
1063  ##| ##5: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
1064  ##]
1065 nqed.
1066
1067 nlemma quintuple_is_comparable :
1068  comparable → comparable → comparable → comparable → comparable → comparable.
1069  #T1; #T2; #T3; #T4; #T5; napply (mk_comparable (Prod5T T1 T2 T3 T4 T5));
1070  ##[ napply (quintuple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4) (zeroc T5))
1071  ##| napply (λP.(forallc T1)
1072              (λe1.(forallc T2)
1073               (λe2.(forallc T3)
1074                (λe3.(forallc T4)
1075                 (λe4.(forallc T5)
1076                  (λe5.P (quintuple … e1 e2 e3 e4 e5)))))))
1077  ##| napply (eq_quintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5))
1078  ##| napply (eqquintuple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1079      ##[ napply (eqc_to_eq T1)
1080      ##| napply (eqc_to_eq T2)
1081      ##| napply (eqc_to_eq T3)
1082      ##| napply (eqc_to_eq T4)
1083      ##| napply (eqc_to_eq T5)
1084      ##]
1085  ##| napply (eq_to_eqquintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1086      ##[ napply (eq_to_eqc T1)
1087      ##| napply (eq_to_eqc T2)
1088      ##| napply (eq_to_eqc T3)
1089      ##| napply (eq_to_eqc T4)
1090      ##| napply (eq_to_eqc T5)
1091      ##]
1092  ##| napply (neqquintuple_to_neq … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1093      ##[ napply (neqc_to_neq T1)
1094      ##| napply (neqc_to_neq T2)
1095      ##| napply (neqc_to_neq T3)
1096      ##| napply (neqc_to_neq T4)
1097      ##| napply (neqc_to_neq T5)
1098      ##]
1099  ##| napply (neq_to_neqquintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1100      ##[ napply (decidable_c T1)
1101      ##| napply (decidable_c T2)
1102      ##| napply (decidable_c T3)
1103      ##| napply (decidable_c T4)
1104      ##| napply (decidable_c T5)
1105      ##| napply (neq_to_neqc T1)
1106      ##| napply (neq_to_neqc T2)
1107      ##| napply (neq_to_neqc T3)
1108      ##| napply (neq_to_neqc T4)
1109      ##| napply (neq_to_neqc T5)
1110      ##]
1111  ##| napply decidable_quintuple;
1112      ##[ napply (decidable_c T1)
1113      ##| napply (decidable_c T2)
1114      ##| napply (decidable_c T3)
1115      ##| napply (decidable_c T4)
1116      ##| napply (decidable_c T5)
1117      ##]
1118  ##| napply symmetric_eqquintuple;
1119      ##[ napply (symmetric_eqc T1)
1120      ##| napply (symmetric_eqc T2)
1121      ##| napply (symmetric_eqc T3)
1122      ##| napply (symmetric_eqc T4)
1123      ##| napply (symmetric_eqc T5)
1124      ##]
1125  ##]
1126 nqed.
1127
1128 unification hint 0 ≔ S1: comparable, S2: comparable, S3: comparable, S4: comparable, S5: comparable;
1129          T1 ≟ (carr S1), T2 ≟ (carr S2), T3 ≟ (carr S3), T4 ≟ (carr S4), T5 ≟ (carr S5),
1130          X ≟ (quintuple_is_comparable S1 S2 S3 S4 S5)
1131  (*********************************************) ⊢
1132          carr X ≡ Prod5T T1 T2 T3 T4 T5.