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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/bool_lemmas.ma".
  24 include "freescale/prod.ma".
  25
  26 (* ***** *)
  27 (* TUPLE *)
  28 (* ***** *)
  29
  30 nlemma pair_destruct_1 :
  31 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  32  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
  33  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  34  nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma pair_destruct_2 :
  41 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  42  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
  43  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  44  nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_eqpair :
  51 ∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
  52 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  53  (symmetricT T1 bool f1) →
  54  (symmetricT T2 bool f2) →
  55  (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
  56  #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
  57  nelim p1;
  58  #x1; #y1;
  59  nelim p2;
  60  #x2; #y2;
  61  nnormalize;
  62  nrewrite > (H x1 x2);
  63  ncases (f1 x2 x1);
  64  nnormalize;
  65  ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
  66  ##| ##2: napply refl_eq
  67  ##]
  68 nqed.
  69
  70 nlemma eq_to_eqpair :
  71 ∀T1,T2.∀p1,p2:ProdT T1 T2.
  72 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  73  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
  74  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
  75  (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
  76  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
  77  nelim p1;
  78  #x1; #y1;
  79  nelim p2;
  80  #x2; #y2; #H;
  81  nnormalize;
  82  nrewrite > (H1 … (pair_destruct_1 … H));
  83  nnormalize;
  84  nrewrite > (H2 … (pair_destruct_2 … H));
  85  napply refl_eq.
  86 nqed.
  87
  88 nlemma eqpair_to_eq :
  89 ∀T1,T2.∀p1,p2:ProdT T1 T2.
  90 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  91  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
  92  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
  93  (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
  94  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
  95  nelim p1;
  96  #x1; #y1;
  97  nelim p2;
  98  #x2; #y2; #H;
  99  nnormalize in H:(%);
 100  nletin K ≝ (H1 x1 x2);
 101  ncases (f1 x1 x2) in H:(%) K:(%);
 102  nnormalize;
 103  #H3;
 104  ##[ ##2: napply (bool_destruct … H3) ##]
 105  #H4;
 106  nrewrite > (H4 (refl_eq …));
 107  nrewrite > (H2 y1 y2 H3);
 108  napply refl_eq.
 109 nqed.
 110
 111 nlemma triple_destruct_1 :
 112 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 113  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
 114  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 115  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
 116  nrewrite < H;
 117  nnormalize;
 118  napply refl_eq.
 119 nqed.
 120
 121 nlemma triple_destruct_2 :
 122 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 123  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
 124  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 125  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
 126  nrewrite < H;
 127  nnormalize;
 128  napply refl_eq.
 129 nqed.
 130
 131 nlemma triple_destruct_3 :
 132 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 133  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
 134  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 135  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
 136  nrewrite < H;
 137  nnormalize;
 138  napply refl_eq.
 139 nqed.
 140
 141 nlemma symmetric_eqtriple :
 142 ∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
 143 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 144  (symmetricT T1 bool f1) →
 145  (symmetricT T2 bool f2) →
 146  (symmetricT T3 bool f3) →
 147  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
 148  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
 149  nelim p1;
 150  #x1; #y1; #z1;
 151  nelim p2;
 152  #x2; #y2; #z2;
 153  nnormalize;
 154  nrewrite > (H x1 x2);
 155  ncases (f1 x2 x1);
 156  nnormalize;
 157  ##[ ##1: nrewrite > (H1 y1 y2);
 158           ncases (f2 y2 y1);
 159           nnormalize;
 160           ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
 161           ##| ##2: napply refl_eq
 162           ##]
 163  ##| ##2: napply refl_eq
 164  ##]
 165 nqed.
 166
 167 nlemma eq_to_eqtriple :
 168 ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
 169 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 170  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 171  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 172  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 173  (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
 174  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
 175  nelim p1;
 176  #x1; #y1; #z1;
 177  nelim p2;
 178  #x2; #y2; #z2; #H;
 179  nnormalize;
 180  nrewrite > (H1 … (triple_destruct_1 … H));
 181  nnormalize;
 182  nrewrite > (H2 … (triple_destruct_2 … H));
 183  nnormalize;
 184  nrewrite > (H3 … (triple_destruct_3 … H));
 185  napply refl_eq.
 186 nqed.
 187
 188 nlemma eqtriple_to_eq :
 189 ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
 190 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 191  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 192  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 193  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 194  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
 195  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
 196  nelim p1;
 197  #x1; #y1; #z1;
 198  nelim p2;
 199  #x2; #y2; #z2; #H;
 200  nnormalize in H:(%);
 201  nletin K ≝ (H1 x1 x2);
 202  ncases (f1 x1 x2) in H:(%) K:(%);
 203  nnormalize;
 204  ##[ ##2: #H4; napply (bool_destruct … H4) ##]
 205  nletin K1 ≝ (H2 y1 y2);
 206  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 207  nnormalize;
 208  ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
 209  #H4; #H5; #H6;
 210  nrewrite > (H4 (refl_eq …));
 211  nrewrite > (H6 (refl_eq …));
 212  nrewrite > (H3 z1 z2 H5);
 213  napply refl_eq.
 214 nqed.
 215
 216 nlemma quadruple_destruct_1 :
 217 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 218  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
 219  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 220  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
 221  nrewrite < H;
 222  nnormalize;
 223  napply refl_eq.
 224 nqed.
 225
 226 nlemma quadruple_destruct_2 :
 227 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 228  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
 229  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 230  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
 231  nrewrite < H;
 232  nnormalize;
 233  napply refl_eq.
 234 nqed.
 235
 236 nlemma quadruple_destruct_3 :
 237 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 238  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
 239  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 240  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
 241  nrewrite < H;
 242  nnormalize;
 243  napply refl_eq.
 244 nqed.
 245
 246 nlemma quadruple_destruct_4 :
 247 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 248  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
 249  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 250  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
 251  nrewrite < H;
 252  nnormalize;
 253  napply refl_eq.
 254 nqed.
 255
 256 nlemma symmetric_eqquadruple :
 257 ∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
 258 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 259  (symmetricT T1 bool f1) →
 260  (symmetricT T2 bool f2) →
 261  (symmetricT T3 bool f3) →
 262  (symmetricT T4 bool f4) →
 263  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
 264  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
 265  nelim p1;
 266  #x1; #y1; #z1; #v1;
 267  nelim p2;
 268  #x2; #y2; #z2; #v2;
 269  nnormalize;
 270  nrewrite > (H x1 x2);
 271  ncases (f1 x2 x1);
 272  nnormalize;
 273  ##[ ##1: nrewrite > (H1 y1 y2);
 274           ncases (f2 y2 y1);
 275           nnormalize;
 276           ##[ ##1: nrewrite > (H2 z1 z2);
 277                    ncases (f3 z2 z1);
 278                    nnormalize;
 279                    ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
 280                    ##| ##2: napply refl_eq
 281                    ##]
 282           ##| ##2: napply refl_eq
 283           ##]
 284  ##| ##2: napply refl_eq
 285  ##]
 286 nqed.
 287
 288 nlemma eq_to_eqquadruple :
 289 ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
 290 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 291  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 292  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 293  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 294  (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
 295  (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
 296  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 297  nelim p1;
 298  #x1; #y1; #z1; #v1;
 299  nelim p2;
 300  #x2; #y2; #z2; #v2; #H;
 301  nnormalize;
 302  nrewrite > (H1 … (quadruple_destruct_1 … H));
 303  nnormalize;
 304  nrewrite > (H2 … (quadruple_destruct_2 … H));
 305  nnormalize;
 306  nrewrite > (H3 … (quadruple_destruct_3 … H));
 307  nnormalize;
 308  nrewrite > (H4 … (quadruple_destruct_4 … H));
 309  napply refl_eq.
 310 nqed.
 311
 312 nlemma eqquadruple_to_eq :
 313 ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
 314 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 315  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 316  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 317  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 318  (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
 319  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
 320  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 321  nelim p1;
 322  #x1; #y1; #z1; #v1;
 323  nelim p2;
 324  #x2; #y2; #z2; #v2; #H;
 325  nnormalize in H:(%);
 326  nletin K ≝ (H1 x1 x2);
 327  ncases (f1 x1 x2) in H:(%) K:(%);
 328  nnormalize;
 329  ##[ ##2: #H5; napply (bool_destruct … H5) ##]
 330  nletin K1 ≝ (H2 y1 y2);
 331  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 332  nnormalize;
 333  ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
 334  nletin K2 ≝ (H3 z1 z2);
 335  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 336  nnormalize;
 337  ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
 338  #H5; #H6; #H7; #H8;
 339  nrewrite > (H5 (refl_eq …));
 340  nrewrite > (H6 (refl_eq …));
 341  nrewrite > (H8 (refl_eq …));
 342  nrewrite > (H4 v1 v2 H7);
 343  napply refl_eq.
 344 nqed.
 345
 346 nlemma quintuple_destruct_1 :
 347 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 348  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
 349  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 350  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
 351  nrewrite < H;
 352  nnormalize;
 353  napply refl_eq.
 354 nqed.
 355
 356 nlemma quintuple_destruct_2 :
 357 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 358  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
 359  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 360  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
 361  nrewrite < H;
 362  nnormalize;
 363  napply refl_eq.
 364 nqed.
 365
 366 nlemma quintuple_destruct_3 :
 367 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 368  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
 369  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 370  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
 371  nrewrite < H;
 372  nnormalize;
 373  napply refl_eq.
 374 nqed.
 375
 376 nlemma quintuple_destruct_4 :
 377 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 378  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
 379  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 380  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
 381  nrewrite < H;
 382  nnormalize;
 383  napply refl_eq.
 384 nqed.
 385
 386 nlemma quintuple_destruct_5 :
 387 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 388  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
 389  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 390  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
 391  nrewrite < H;
 392  nnormalize;
 393  napply refl_eq.
 394 nqed.
 395
 396 nlemma symmetric_eqquintuple :
 397 ∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 398 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 399  (symmetricT T1 bool f1) →
 400  (symmetricT T2 bool f2) →
 401  (symmetricT T3 bool f3) →
 402  (symmetricT T4 bool f4) →
 403  (symmetricT T5 bool f5) →
 404  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
 405  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
 406  nelim p1;
 407  #x1; #y1; #z1; #v1; #w1;
 408  nelim p2;
 409  #x2; #y2; #z2; #v2; #w2;
 410  nnormalize;
 411  nrewrite > (H x1 x2);
 412  ncases (f1 x2 x1);
 413  nnormalize;
 414  ##[ ##1: nrewrite > (H1 y1 y2);
 415           ncases (f2 y2 y1);
 416           nnormalize;
 417           ##[ ##1: nrewrite > (H2 z1 z2);
 418                    ncases (f3 z2 z1);
 419                    nnormalize;
 420                    ##[ ##1: nrewrite > (H3 v1 v2);
 421                             ncases (f4 v2 v1);
 422                             nnormalize;
 423                             ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
 424                             ##| ##2: napply refl_eq
 425                             ##]
 426                    ##| ##2: napply refl_eq
 427                    ##]
 428           ##| ##2: napply refl_eq
 429           ##]
 430  ##| ##2: napply refl_eq
 431  ##]
 432 nqed.
 433
 434 nlemma eq_to_eqquintuple :
 435 ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 436 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 437  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 438  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 439  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 440  (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
 441  (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
 442  (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
 443  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 444  nelim p1;
 445  #x1; #y1; #z1; #v1; #w1;
 446  nelim p2;
 447  #x2; #y2; #z2; #v2; #w2; #H;
 448  nnormalize;
 449  nrewrite > (H1 … (quintuple_destruct_1 … H));
 450  nnormalize;
 451  nrewrite > (H2 … (quintuple_destruct_2 … H));
 452  nnormalize;
 453  nrewrite > (H3 … (quintuple_destruct_3 … H));
 454  nnormalize;
 455  nrewrite > (H4 … (quintuple_destruct_4 … H));
 456  nnormalize;
 457  nrewrite > (H5 … (quintuple_destruct_5 … H));
 458  napply refl_eq.
 459 nqed.
 460
 461 nlemma eqquintuple_to_eq :
 462 ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 463 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 464  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 465  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 466  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 467  (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
 468  (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
 469  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
 470  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 471  nelim p1;
 472  #x1; #y1; #z1; #v1; #w1;
 473  nelim p2;
 474  #x2; #y2; #z2; #v2; #w2; #H;
 475  nnormalize in H:(%);
 476  nletin K ≝ (H1 x1 x2);
 477  ncases (f1 x1 x2) in H:(%) K:(%);
 478  nnormalize;
 479  ##[ ##2: #H6; napply (bool_destruct … H6) ##]
 480  nletin K1 ≝ (H2 y1 y2);
 481  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 482  nnormalize;
 483  ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
 484  nletin K2 ≝ (H3 z1 z2);
 485  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 486  nnormalize;
 487  ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
 488  nletin K3 ≝ (H4 v1 v2);
 489  ncases (f4 v1 v2) in K3:(%) ⊢ %;
 490  nnormalize;
 491  ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
 492  #H6; #H7; #H8; #H9; #H10;
 493  nrewrite > (H6 (refl_eq …));
 494  nrewrite > (H7 (refl_eq …));
 495  nrewrite > (H8 (refl_eq …));
 496  nrewrite > (H10 (refl_eq …));
 497  nrewrite > (H5 w1 w2 H9);
 498  napply refl_eq.
 499 nqed.