]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
freescale porting, work in progress
[helm.git] / 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.