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