1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool_lemmas.ma".
28 include "freescale/prod.ma".
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 ]);
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 ]);
54 nlemma symmetric_eqpair :
55 ∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
56 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
57 (symmetricT T1 bool f1) →
58 (symmetricT T2 bool 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 napply (ProdT_ind T1 T2 ?? p1);
63 napply (ProdT_ind T1 T2 ?? p2);
69 ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
70 ##| ##2: napply (refl_eq ??)
75 ∀T1,T2.∀p1,p2:ProdT T1 T2.
76 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
77 (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
78 (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
79 (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
80 #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
81 napply (ProdT_ind T1 T2 ?? p1);
83 napply (ProdT_ind T1 T2 ?? p2);
86 nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
88 nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
93 ∀T1,T2.∀p1,p2:ProdT T1 T2.
94 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
95 (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
96 (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
97 (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
98 #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
99 napply (ProdT_ind T1 T2 ?? p1);
101 napply (ProdT_ind T1 T2 ?? p2);
104 nletin K ≝ (H1 x1 x2);
105 ncases (f1 x1 x2) in H:(%) K:(%);
108 ##[ ##2: napply (bool_destruct ??? H3) ##]
110 nrewrite > (H4 (refl_eq ??));
111 nrewrite > (H2 y1 y2 H3);
115 nlemma triple_destruct_1 :
116 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
117 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
118 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
119 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
125 nlemma triple_destruct_2 :
126 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
127 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
128 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
129 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
135 nlemma triple_destruct_3 :
136 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
137 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
138 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
139 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
145 nlemma symmetric_eqtriple :
146 ∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
147 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
148 (symmetricT T1 bool f1) →
149 (symmetricT T2 bool f2) →
150 (symmetricT T3 bool f3) →
151 (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
152 #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
153 napply (Prod3T_ind T1 T2 T3 ?? p1);
155 napply (Prod3T_ind T1 T2 T3 ?? p2);
158 nrewrite > (H x1 x2);
161 ##[ ##1: nrewrite > (H1 y1 y2);
164 ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
165 ##| ##2: napply (refl_eq ??)
167 ##| ##2: napply (refl_eq ??)
171 nlemma eq_to_eqtriple :
172 ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
173 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
174 (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
175 (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
176 (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
177 (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
178 #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
179 napply (Prod3T_ind T1 T2 T3 ?? p1);
181 napply (Prod3T_ind T1 T2 T3 ?? p2);
184 nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
186 nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
188 nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
192 nlemma eqtriple_to_eq :
193 ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
194 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
195 (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
196 (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
197 (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
198 (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
199 #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
200 napply (Prod3T_ind T1 T2 T3 ?? p1);
202 napply (Prod3T_ind T1 T2 T3 ?? p2);
205 nletin K ≝ (H1 x1 x2);
206 ncases (f1 x1 x2) in H:(%) K:(%);
208 ##[ ##2: #H4; napply (bool_destruct ??? H4) ##]
209 nletin K1 ≝ (H2 y1 y2);
210 ncases (f2 y1 y2) in K1:(%) ⊢ %;
212 ##[ ##2: #H4; #H5; napply (bool_destruct ??? H5) ##]
214 nrewrite > (H4 (refl_eq ??));
215 nrewrite > (H6 (refl_eq ??));
216 nrewrite > (H3 z1 z2 H5);
220 nlemma quadruple_destruct_1 :
221 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
222 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
223 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
224 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
230 nlemma quadruple_destruct_2 :
231 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
232 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
233 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
234 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
240 nlemma quadruple_destruct_3 :
241 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
242 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
243 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
244 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
250 nlemma quadruple_destruct_4 :
251 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
252 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
253 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
254 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
260 nlemma symmetric_eqquadruple :
261 ∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
262 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
263 (symmetricT T1 bool f1) →
264 (symmetricT T2 bool f2) →
265 (symmetricT T3 bool f3) →
266 (symmetricT T4 bool f4) →
267 (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
268 #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
269 napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
271 napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
274 nrewrite > (H x1 x2);
277 ##[ ##1: nrewrite > (H1 y1 y2);
280 ##[ ##1: nrewrite > (H2 z1 z2);
283 ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
284 ##| ##2: napply (refl_eq ??)
286 ##| ##2: napply (refl_eq ??)
288 ##| ##2: napply (refl_eq ??)
292 nlemma eq_to_eqquadruple :
293 ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
294 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
295 (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
296 (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
297 (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
298 (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
299 (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
300 #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
301 napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
303 napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
304 #x2; #y2; #z2; #v2; #H;
306 nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
308 nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
310 nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
312 nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
316 nlemma eqquadruple_to_eq :
317 ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
318 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
319 (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
320 (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
321 (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
322 (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
323 (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
324 #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
325 napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
327 napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
328 #x2; #y2; #z2; #v2; #H;
330 nletin K ≝ (H1 x1 x2);
331 ncases (f1 x1 x2) in H:(%) K:(%);
333 ##[ ##2: #H5; napply (bool_destruct ??? H5) ##]
334 nletin K1 ≝ (H2 y1 y2);
335 ncases (f2 y1 y2) in K1:(%) ⊢ %;
337 ##[ ##2: #H5; #H6; napply (bool_destruct ??? H6) ##]
338 nletin K2 ≝ (H3 z1 z2);
339 ncases (f3 z1 z2) in K2:(%) ⊢ %;
341 ##[ ##2: #H5; #H6; #H7; napply (bool_destruct ??? H7) ##]
343 nrewrite > (H5 (refl_eq ??));
344 nrewrite > (H6 (refl_eq ??));
345 nrewrite > (H8 (refl_eq ??));
346 nrewrite > (H4 v1 v2 H7);
350 nlemma quintuple_destruct_1 :
351 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
352 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
353 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
354 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
360 nlemma quintuple_destruct_2 :
361 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
362 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
363 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
364 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
370 nlemma quintuple_destruct_3 :
371 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
372 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
373 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
374 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
380 nlemma quintuple_destruct_4 :
381 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
382 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
383 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
384 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
390 nlemma quintuple_destruct_5 :
391 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
392 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
393 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
394 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
400 nlemma symmetric_eqquintuple :
401 ∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
402 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
403 (symmetricT T1 bool f1) →
404 (symmetricT T2 bool f2) →
405 (symmetricT T3 bool f3) →
406 (symmetricT T4 bool f4) →
407 (symmetricT T5 bool f5) →
408 (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).
409 #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
410 napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
411 #x1; #y1; #z1; #v1; #w1;
412 napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
413 #x2; #y2; #z2; #v2; #w2;
415 nrewrite > (H x1 x2);
418 ##[ ##1: nrewrite > (H1 y1 y2);
421 ##[ ##1: nrewrite > (H2 z1 z2);
424 ##[ ##1: nrewrite > (H3 v1 v2);
427 ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
428 ##| ##2: napply (refl_eq ??)
430 ##| ##2: napply (refl_eq ??)
432 ##| ##2: napply (refl_eq ??)
434 ##| ##2: napply (refl_eq ??)
438 nlemma eq_to_eqquintuple :
439 ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
440 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
441 (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
442 (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
443 (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
444 (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
445 (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
446 (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
447 #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
448 napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
449 #x1; #y1; #z1; #v1; #w1;
450 napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
451 #x2; #y2; #z2; #v2; #w2; #H;
453 nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
455 nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
457 nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
459 nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
461 nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
465 nlemma eqquintuple_to_eq :
466 ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
467 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
468 (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
469 (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
470 (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
471 (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
472 (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
473 (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
474 #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
475 napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
476 #x1; #y1; #z1; #v1; #w1;
477 napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
478 #x2; #y2; #z2; #v2; #w2; #H;
480 nletin K ≝ (H1 x1 x2);
481 ncases (f1 x1 x2) in H:(%) K:(%);
483 ##[ ##2: #H6; napply (bool_destruct ??? H6) ##]
484 nletin K1 ≝ (H2 y1 y2);
485 ncases (f2 y1 y2) in K1:(%) ⊢ %;
487 ##[ ##2: #H6; #H7; napply (bool_destruct ??? H7) ##]
488 nletin K2 ≝ (H3 z1 z2);
489 ncases (f3 z1 z2) in K2:(%) ⊢ %;
491 ##[ ##2: #H6; #H7; #H8; napply (bool_destruct ??? H8) ##]
492 nletin K3 ≝ (H4 v1 v2);
493 ncases (f4 v1 v2) in K3:(%) ⊢ %;
495 ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct ??? H9) ##]
496 #H6; #H7; #H8; #H9; #H10;
497 nrewrite > (H6 (refl_eq ??));
498 nrewrite > (H7 (refl_eq ??));
499 nrewrite > (H8 (refl_eq ??));
500 nrewrite > (H10 (refl_eq ??));
501 nrewrite > (H5 w1 w2 H9);