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