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 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;
68 ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
69 ##| ##2: napply (refl_eq ??)
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;
82 #x2; #y2; #x1; #y1; #H;
84 nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
86 nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
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;
99 #x2; #y2; #x1; #y1; #H;
101 nletin K ≝ (H1 x1 x2);
102 ncases (f1 x1 x2) in H:(%) K:(%);
105 ##[ ##2: nelim (bool_destruct_false_true H3) ##]
107 nrewrite > (H4 (refl_eq ??));
108 nrewrite > (H2 y1 y2 H3);
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 ]);
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 ]);
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 ]);
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;
152 #x2; #y2; #z2; #x1; #y1; #z1;
154 nrewrite > (H x1 x2);
157 ##[ ##1: nrewrite > (H1 y1 y2);
160 ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
161 ##| ##2: napply (refl_eq ??)
163 ##| ##2: napply (refl_eq ??)
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;
177 #x2; #y2; #z2; #x1; #y1; #z1; #H;
179 nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
181 nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
183 nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
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;
197 #x2; #y2; #z2; #x1; #y1; #z1; #H;
199 nletin K ≝ (H1 x1 x2);
200 ncases (f1 x1 x2) in H:(%) K:(%);
202 ##[ ##2: #H4; nelim (bool_destruct_false_true H4) ##]
203 nletin K1 ≝ (H2 y1 y2);
204 ncases (f2 y1 y2) in K1:(%) ⊢ %;
206 ##[ ##2: #H4; #H5; nelim (bool_destruct_false_true H5) ##]
208 nrewrite > (H4 (refl_eq ??));
209 nrewrite > (H6 (refl_eq ??));
210 nrewrite > (H3 z1 z2 H5);
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 ]);
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 ]);
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 ]);
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 ]);
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;
265 #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1;
267 nrewrite > (H x1 x2);
270 ##[ ##1: nrewrite > (H1 y1 y2);
273 ##[ ##1: nrewrite > (H2 z1 z2);
276 ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
277 ##| ##2: napply (refl_eq ??)
279 ##| ##2: napply (refl_eq ??)
281 ##| ##2: napply (refl_eq ??)
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;
296 #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
298 nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
300 nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
302 nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
304 nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
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;
319 #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
321 nletin K ≝ (H1 x1 x2);
322 ncases (f1 x1 x2) in H:(%) K:(%);
324 ##[ ##2: #H5; nelim (bool_destruct_false_true H5) ##]
325 nletin K1 ≝ (H2 y1 y2);
326 ncases (f2 y1 y2) in K1:(%) ⊢ %;
328 ##[ ##2: #H5; #H6; nelim (bool_destruct_false_true H6) ##]
329 nletin K2 ≝ (H3 z1 z2);
330 ncases (f3 z1 z2) in K2:(%) ⊢ %;
332 ##[ ##2: #H5; #H6; #H7; nelim (bool_destruct_false_true H7) ##]
334 nrewrite > (H5 (refl_eq ??));
335 nrewrite > (H6 (refl_eq ??));
336 nrewrite > (H8 (refl_eq ??));
337 nrewrite > (H4 v1 v2 H7);
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 ]);
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 ]);
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 ]);
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 ]);
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 ]);
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;
403 #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1;
405 nrewrite > (H x1 x2);
408 ##[ ##1: nrewrite > (H1 y1 y2);
411 ##[ ##1: nrewrite > (H2 z1 z2);
414 ##[ ##1: nrewrite > (H3 v1 v2);
417 ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
418 ##| ##2: napply (refl_eq ??)
420 ##| ##2: napply (refl_eq ??)
422 ##| ##2: napply (refl_eq ??)
424 ##| ##2: napply (refl_eq ??)
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;
440 #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
442 nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
444 nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
446 nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
448 nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
450 nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
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;
466 #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
468 nletin K ≝ (H1 x1 x2);
469 ncases (f1 x1 x2) in H:(%) K:(%);
471 ##[ ##2: #H6; nelim (bool_destruct_false_true H6) ##]
472 nletin K1 ≝ (H2 y1 y2);
473 ncases (f2 y1 y2) in K1:(%) ⊢ %;
475 ##[ ##2: #H6; #H7; nelim (bool_destruct_false_true H7) ##]
476 nletin K2 ≝ (H3 z1 z2);
477 ncases (f3 z1 z2) in K2:(%) ⊢ %;
479 ##[ ##2: #H6; #H7; #H8; nelim (bool_destruct_false_true H8) ##]
480 nletin K3 ≝ (H4 v1 v2);
481 ncases (f4 v1 v2) in K3:(%) ⊢ %;
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);