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 *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/prod.ma".
24 include "num/bool_lemmas.ma".
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 ]);
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 ]);
50 nlemma symmetric_eqpair :
52 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
53 (symmetricT T1 bool f1) →
54 (symmetricT T2 bool f2) →
56 (eq_pair T1 T2 f1 f2 p1 p2 = eq_pair T1 T2 f1 f2 p1 p2)).
57 #T1; #T2; #f1; #f2; #H; #H1;
58 #p1; nelim p1; #x1; #y1;
59 #p2; nelim p2; #x2; #y2;
64 ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
65 ##| ##2: napply refl_eq
71 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
72 (∀x,y:T1.x = y → f1 x y = true) →
73 (∀x,y:T2.x = y → f2 x y = true) →
75 (p1 = p2 → eq_pair T1 T2 f1 f2 p1 p2 = true)).
76 #T1; #T2; #f1; #f2; #H1; #H2;
77 #p1; nelim p1; #x1; #y1;
78 #p2; nelim p2; #x2; #y2; #H;
80 nrewrite > (H1 … (pair_destruct_1 … H));
82 nrewrite > (H2 … (pair_destruct_2 … H));
88 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
89 (∀x,y:T1.f1 x y = true → x = y) →
90 (∀x,y:T2.f2 x y = true → x = y) →
92 (eq_pair T1 T2 f1 f2 p1 p2 = true → p1 = p2)).
93 #T1; #T2; #f1; #f2; #H1; #H2;
94 #p1; nelim p1; #x1; #y1;
95 #p2; nelim p2; #x2; #y2; #H;
97 nletin K ≝ (H1 x1 x2);
98 ncases (f1 x1 x2) in H:(%) K:(%);
101 ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
103 nrewrite > (H4 (refl_eq …));
104 nrewrite > (H2 y1 y2 H3);
108 nlemma decidable_pair :
110 (∀x,y:T1.decidable (x = y)) →
111 (∀x,y:T2.decidable (x = y)) →
112 (∀x,y:ProdT T1 T2.decidable (x = y)).
114 #x; nelim x; #xx1; #xx2;
115 #y; nelim y; #yy1; #yy2;
117 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
118 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
119 nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
120 ##| ##1: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
121 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
122 nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
123 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
124 nrewrite > H2; nrewrite > H3; napply refl_eq
129 nlemma neqpair_to_neq :
131 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
132 (∀x,y:T1.f1 x y = false → x ≠ y) →
133 (∀x,y:T2.f2 x y = false → x ≠ y) →
135 (eq_pair T1 T2 f1 f2 p1 p2 = false → p1 ≠ p2)).
136 #T1; #T2; #f1; #f2; #H1; #H2;
137 #p1; nelim p1; #x1; #y1;
138 #p2; nelim p2; #x2; #y2;
139 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
141 napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
142 ##[ ##1: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
143 ##| ##2: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
147 nlemma pair_destruct :
149 (∀x,y:T1.decidable (x = y)) →
150 (∀x,y:T2.decidable (x = y)) →
151 (∀x1,x2:T1.∀y1,y2:T2.
152 (pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2).
153 #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
155 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
156 ##[ ##2: #H3; napply (or2_intro1 … H3)
157 ##| ##1: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
158 ##[ ##2: #H4; napply (or2_intro2 … H4)
159 ##| ##1: #H4; nrewrite > H3 in H:(%);
160 nrewrite > H4; #H; nelim (H (refl_eq …))
165 nlemma neq_to_neqpair :
167 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
168 (∀x,y:T1.decidable (x = y)) →
169 (∀x,y:T2.decidable (x = y)) →
170 (∀x,y:T1.x ≠ y → f1 x y = false) →
171 (∀x,y:T2.x ≠ y → f2 x y = false) →
173 (p1 ≠ p2 → eq_pair T1 T2 f1 f2 p1 p2 = false)).
174 #T1; #T2; #f1; #f2; #H1; #H2; #H3; #H4;
175 #p1; nelim p1; #x1; #y1;
176 #p2; nelim p2; #x2; #y2; #H;
177 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
178 napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
179 ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
180 ##| ##1: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
188 nlemma triple_destruct_1 :
189 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
190 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
191 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
192 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
198 nlemma triple_destruct_2 :
199 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
200 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
201 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
202 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
208 nlemma triple_destruct_3 :
209 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
210 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
211 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
212 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
218 nlemma symmetric_eqtriple :
220 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
221 (symmetricT T1 bool f1) →
222 (symmetricT T2 bool f2) →
223 (symmetricT T3 bool f3) →
224 (∀p1,p2:Prod3T T1 T2 T3.
225 (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = eq_triple T1 T2 T3 f1 f2 f3 p2 p1)).
226 #T1; #T2; #T3; #f1; #f2; #f3; #H; #H1; #H2;
227 #p1; nelim p1; #x1; #y1; #z1;
228 #p2; nelim p2; #x2; #y2; #z2;
230 nrewrite > (H x1 x2);
233 ##[ ##1: nrewrite > (H1 y1 y2);
236 ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
237 ##| ##2: napply refl_eq
239 ##| ##2: napply refl_eq
243 nlemma eq_to_eqtriple :
245 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
246 (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
247 (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
248 (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
249 (∀p1,p2:Prod3T T1 T2 T3.
250 (p1 = p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true)).
251 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
252 #p1; nelim p1; #x1; #y1; #z1;
253 #p2; nelim p2; #x2; #y2; #z2; #H;
255 nrewrite > (H1 … (triple_destruct_1 … H));
257 nrewrite > (H2 … (triple_destruct_2 … H));
259 nrewrite > (H3 … (triple_destruct_3 … H));
263 nlemma eqtriple_to_eq :
265 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
266 (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
267 (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
268 (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
269 (∀p1,p2:Prod3T T1 T2 T3.
270 (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true → p1 = p2)).
271 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
272 #p1; nelim p1; #x1; #y1; #z1;
273 #p2; nelim p2; #x2; #y2; #z2; #H;
275 nletin K ≝ (H1 x1 x2);
276 ncases (f1 x1 x2) in H:(%) K:(%);
278 ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
279 nletin K1 ≝ (H2 y1 y2);
280 ncases (f2 y1 y2) in K1:(%) ⊢ %;
282 ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
284 nrewrite > (H4 (refl_eq …));
285 nrewrite > (H6 (refl_eq …));
286 nrewrite > (H3 z1 z2 H5);
290 nlemma decidable_triple :
292 (∀x,y:T1.decidable (x = y)) →
293 (∀x,y:T2.decidable (x = y)) →
294 (∀x,y:T3.decidable (x = y)) →
295 (∀x,y:Prod3T T1 T2 T3.decidable (x = y)).
296 #T1; #T2; #T3; #H; #H1; #H2;
297 #x; nelim x; #xx1; #xx2; #xx3;
298 #y; nelim y; #yy1; #yy2; #yy3;
300 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
301 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
302 nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
303 ##| ##1: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
304 ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
305 nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
306 ##| ##1: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
307 ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
308 nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
309 ##| ##1: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
319 nlemma neqtriple_to_neq :
321 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
322 (∀x,y:T1.f1 x y = false → x ≠ y) →
323 (∀x,y:T2.f2 x y = false → x ≠ y) →
324 (∀x,y:T3.f3 x y = false → x ≠ y) →
325 (∀p1,p2:Prod3T T1 T2 T3.
326 (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false → p1 ≠ p2)).
327 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
328 #p1; nelim p1; #x1; #y1; #z1;
329 #p2; nelim p2; #x2; #y2; #z2;
330 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
332 napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
333 ##[ ##1: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
334 ##| ##2: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
335 ##| ##3: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
339 nlemma triple_destruct :
341 (∀x,y:T1.decidable (x = y)) →
342 (∀x,y:T2.decidable (x = y)) →
343 (∀x,y:T3.decidable (x = y)) →
344 (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
345 (triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
346 Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2)).
347 #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
349 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
350 ##[ ##2: #H4; napply (or3_intro1 … H4)
351 ##| ##1: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
352 ##[ ##2: #H5; napply (or3_intro2 … H5)
353 ##| ##1: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
354 ##[ ##2: #H6; napply (or3_intro3 … H6)
355 ##| ##1: #H6; nrewrite > H4 in H:(%);
357 nrewrite > H6; #H; nelim (H (refl_eq …))
363 nlemma neq_to_neqtriple :
365 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
366 (∀x,y:T1.decidable (x = y)) →
367 (∀x,y:T2.decidable (x = y)) →
368 (∀x,y:T3.decidable (x = y)) →
369 (∀x,y:T1.x ≠ y → f1 x y = false) →
370 (∀x,y:T2.x ≠ y → f2 x y = false) →
371 (∀x,y:T3.x ≠ y → f3 x y = false) →
372 (∀p1,p2:Prod3T T1 T2 T3.
373 (p1 ≠ p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false)).
374 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
375 #p1; nelim p1; #x1; #y1; #z1;
376 #p2; nelim p2; #x2; #y2; #z2; #H;
377 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
378 napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
379 ##[ ##1: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
380 ##| ##2: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
381 ##| ##3: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
389 nlemma quadruple_destruct_1 :
390 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
391 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
392 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
393 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
399 nlemma quadruple_destruct_2 :
400 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
401 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
402 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
403 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
409 nlemma quadruple_destruct_3 :
410 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
411 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
412 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
413 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
419 nlemma quadruple_destruct_4 :
420 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
421 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
422 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
423 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
429 nlemma symmetric_eqquadruple :
431 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
432 (symmetricT T1 bool f1) →
433 (symmetricT T2 bool f2) →
434 (symmetricT T3 bool f3) →
435 (symmetricT T4 bool f4) →
436 (∀p1,p2:Prod4T T1 T2 T3 T4.
437 (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p2 p1)).
438 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
439 #p1; nelim p1; #x1; #y1; #z1; #v1;
440 #p2; nelim p2; #x2; #y2; #z2; #v2;
442 nrewrite > (H x1 x2);
445 ##[ ##1: nrewrite > (H1 y1 y2);
448 ##[ ##1: nrewrite > (H2 z1 z2);
451 ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
452 ##| ##2: napply refl_eq
454 ##| ##2: napply refl_eq
456 ##| ##2: napply refl_eq
460 nlemma eq_to_eqquadruple :
462 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
463 (∀x,y:T1.x = y → f1 x y = true) →
464 (∀x,y:T2.x = y → f2 x y = true) →
465 (∀x,y:T3.x = y → f3 x y = true) →
466 (∀x,y:T4.x = y → f4 x y = true) →
467 (∀p1,p2:Prod4T T1 T2 T3 T4.
468 (p1 = p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true)).
469 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
470 #p1; nelim p1; #x1; #y1; #z1; #v1;
471 #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
473 nrewrite > (H1 … (quadruple_destruct_1 … H));
475 nrewrite > (H2 … (quadruple_destruct_2 … H));
477 nrewrite > (H3 … (quadruple_destruct_3 … H));
479 nrewrite > (H4 … (quadruple_destruct_4 … H));
483 nlemma eqquadruple_to_eq :
485 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
486 (∀x,y:T1.f1 x y = true → x = y) →
487 (∀x,y:T2.f2 x y = true → x = y) →
488 (∀x,y:T3.f3 x y = true → x = y) →
489 (∀x,y:T4.f4 x y = true → x = y) →
490 (∀p1,p2:Prod4T T1 T2 T3 T4.
491 (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true → p1 = p2)).
492 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
493 #p1; nelim p1; #x1; #y1; #z1; #v1;
494 #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
496 nletin K ≝ (H1 x1 x2);
497 ncases (f1 x1 x2) in H:(%) K:(%);
499 ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
500 nletin K1 ≝ (H2 y1 y2);
501 ncases (f2 y1 y2) in K1:(%) ⊢ %;
503 ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
504 nletin K2 ≝ (H3 z1 z2);
505 ncases (f3 z1 z2) in K2:(%) ⊢ %;
507 ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
509 nrewrite > (H5 (refl_eq …));
510 nrewrite > (H6 (refl_eq …));
511 nrewrite > (H8 (refl_eq …));
512 nrewrite > (H4 v1 v2 H7);
516 nlemma decidable_quadruple :
518 (∀x,y:T1.decidable (x = y)) →
519 (∀x,y:T2.decidable (x = y)) →
520 (∀x,y:T3.decidable (x = y)) →
521 (∀x,y:T4.decidable (x = y)) →
522 (∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y)).
523 #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3;
524 #x; nelim x; #xx1; #xx2; #xx3; #xx4;
525 #y; nelim y; #yy1; #yy2; #yy3; #yy4;
527 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
528 ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
529 nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
530 ##| ##1: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
531 ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
532 nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
533 ##| ##1: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
534 ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
535 nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
536 ##| ##1: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
537 ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
538 nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
539 ##| ##1: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
551 nlemma neqquadruple_to_neq :
553 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
554 (∀x,y:T1.f1 x y = false → x ≠ y) →
555 (∀x,y:T2.f2 x y = false → x ≠ y) →
556 (∀x,y:T3.f3 x y = false → x ≠ y) →
557 (∀x,y:T4.f4 x y = false → x ≠ y) →
558 (∀p1,p2:Prod4T T1 T2 T3 T4.
559 (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false → p1 ≠ p2)).
560 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
561 #p1; nelim p1; #x1; #y1; #z1; #v1;
562 #p2; nelim p2; #x2; #y2; #z2; #v2;
563 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
565 napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
566 ##[ ##1: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
567 ##| ##2: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
568 ##| ##3: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
569 ##| ##4: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
573 nlemma quadruple_destruct :
575 (∀x,y:T1.decidable (x = y)) →
576 (∀x,y:T2.decidable (x = y)) →
577 (∀x,y:T3.decidable (x = y)) →
578 (∀x,y:T4.decidable (x = y)) →
579 (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
580 (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
581 Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2)).
582 #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4;
583 #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
585 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
586 ##[ ##2: #H5; napply (or4_intro1 … H5)
587 ##| ##1: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
588 ##[ ##2: #H6; napply (or4_intro2 … H6)
589 ##| ##1: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
590 ##[ ##2: #H7; napply (or4_intro3 … H7)
591 ##| ##1: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
592 ##[ ##2: #H8; napply (or4_intro4 … H8)
593 ##| ##1: #H8; nrewrite > H5 in H:(%);
596 nrewrite > H8; #H; nelim (H (refl_eq …))
603 nlemma neq_to_neqquadruple :
605 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
606 (∀x,y:T1.decidable (x = y)) →
607 (∀x,y:T2.decidable (x = y)) →
608 (∀x,y:T3.decidable (x = y)) →
609 (∀x,y:T4.decidable (x = y)) →
610 (∀x,y:T1.x ≠ y → f1 x y = false) →
611 (∀x,y:T2.x ≠ y → f2 x y = false) →
612 (∀x,y:T3.x ≠ y → f3 x y = false) →
613 (∀x,y:T4.x ≠ y → f4 x y = false) →
614 (∀p1,p2:Prod4T T1 T2 T3 T4.
615 (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false)).
616 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
617 #p1; nelim p1; #x1; #y1; #z1; #v1;
618 #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
619 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
620 napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
621 ##[ ##1: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
622 ##| ##2: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
623 ##| ##3: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
624 ##| ##4: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
632 nlemma quintuple_destruct_1 :
633 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
634 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
635 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
636 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
642 nlemma quintuple_destruct_2 :
643 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
644 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
645 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
646 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
652 nlemma quintuple_destruct_3 :
653 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
654 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
655 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
656 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
662 nlemma quintuple_destruct_4 :
663 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
664 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
665 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
666 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
672 nlemma quintuple_destruct_5 :
673 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
674 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
675 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
676 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
682 nlemma symmetric_eqquintuple :
683 ∀T1,T2,T3,T4,T5:Type.
684 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
685 (symmetricT T1 bool f1) →
686 (symmetricT T2 bool f2) →
687 (symmetricT T3 bool f3) →
688 (symmetricT T4 bool f4) →
689 (symmetricT T5 bool f5) →
690 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
691 (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p2 p1)).
692 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
693 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
694 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
696 nrewrite > (H x1 x2);
699 ##[ ##1: nrewrite > (H1 y1 y2);
702 ##[ ##1: nrewrite > (H2 z1 z2);
705 ##[ ##1: nrewrite > (H3 v1 v2);
708 ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
709 ##| ##2: napply refl_eq
711 ##| ##2: napply refl_eq
713 ##| ##2: napply refl_eq
715 ##| ##2: napply refl_eq
719 nlemma eq_to_eqquintuple :
721 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
722 (∀x,y:T1.x = y → f1 x y = true) →
723 (∀x,y:T2.x = y → f2 x y = true) →
724 (∀x,y:T3.x = y → f3 x y = true) →
725 (∀x,y:T4.x = y → f4 x y = true) →
726 (∀x,y:T5.x = y → f5 x y = true) →
727 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
728 (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true)).
729 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
730 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
731 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
733 nrewrite > (H1 … (quintuple_destruct_1 … H));
735 nrewrite > (H2 … (quintuple_destruct_2 … H));
737 nrewrite > (H3 … (quintuple_destruct_3 … H));
739 nrewrite > (H4 … (quintuple_destruct_4 … H));
741 nrewrite > (H5 … (quintuple_destruct_5 … H));
745 nlemma eqquintuple_to_eq :
747 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
748 (∀x,y:T1.f1 x y = true → x = y) →
749 (∀x,y:T2.f2 x y = true → x = y) →
750 (∀x,y:T3.f3 x y = true → x = y) →
751 (∀x,y:T4.f4 x y = true → x = y) →
752 (∀x,y:T5.f5 x y = true → x = y) →
753 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
754 (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true → p1 = p2)).
755 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
756 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
757 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
759 nletin K ≝ (H1 x1 x2);
760 ncases (f1 x1 x2) in H:(%) K:(%);
762 ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
763 nletin K1 ≝ (H2 y1 y2);
764 ncases (f2 y1 y2) in K1:(%) ⊢ %;
766 ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
767 nletin K2 ≝ (H3 z1 z2);
768 ncases (f3 z1 z2) in K2:(%) ⊢ %;
770 ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
771 nletin K3 ≝ (H4 v1 v2);
772 ncases (f4 v1 v2) in K3:(%) ⊢ %;
774 ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
775 #H6; #H7; #H8; #H9; #H10;
776 nrewrite > (H6 (refl_eq …));
777 nrewrite > (H7 (refl_eq …));
778 nrewrite > (H8 (refl_eq …));
779 nrewrite > (H10 (refl_eq …));
780 nrewrite > (H5 w1 w2 H9);
784 nlemma decidable_quintuple :
786 (∀x,y:T1.decidable (x = y)) →
787 (∀x,y:T2.decidable (x = y)) →
788 (∀x,y:T3.decidable (x = y)) →
789 (∀x,y:T4.decidable (x = y)) →
790 (∀x,y:T5.decidable (x = y)) →
791 (∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y)).
792 #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4;
793 #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5;
794 #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
796 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
797 ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
798 nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
799 ##| ##1: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
800 ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
801 nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
802 ##| ##1: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
803 ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
804 nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
805 ##| ##1: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
806 ##[ ##2: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
807 nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
808 ##| ##1: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
809 ##[ ##2: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
810 nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
811 ##| ##1: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
825 nlemma neqquintuple_to_neq :
827 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
828 (∀x,y:T1.f1 x y = false → x ≠ y) →
829 (∀x,y:T2.f2 x y = false → x ≠ y) →
830 (∀x,y:T3.f3 x y = false → x ≠ y) →
831 (∀x,y:T4.f4 x y = false → x ≠ y) →
832 (∀x,y:T5.f5 x y = false → x ≠ y) →
833 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
834 (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false → p1 ≠ p2)).
835 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
836 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
837 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
838 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
840 napply (or5_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ((f5 w1 w2) = false) ? (andb_false5 … H) ?);
841 ##[ ##1: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
842 ##| ##2: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
843 ##| ##3: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
844 ##| ##4: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
845 ##| ##5: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
849 nlemma quintuple_destruct :
851 (∀x,y:T1.decidable (x = y)) →
852 (∀x,y:T2.decidable (x = y)) →
853 (∀x,y:T3.decidable (x = y)) →
854 (∀x,y:T4.decidable (x = y)) →
855 (∀x,y:T5.decidable (x = y)) →
856 (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
857 (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
858 Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2)).
859 #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5;
860 #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
862 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
863 ##[ ##2: #H6; napply (or5_intro1 … H6)
864 ##| ##1: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
865 ##[ ##2: #H7; napply (or5_intro2 … H7)
866 ##| ##1: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
867 ##[ ##2: #H8; napply (or5_intro3 … H8)
868 ##| ##1: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
869 ##[ ##2: #H9; napply (or5_intro4 … H9)
870 ##| ##1: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
871 ##[ ##2: #H10; napply (or5_intro5 … H10)
872 ##| ##1: #H10; nrewrite > H6 in H:(%);
876 nrewrite > H10; #H; nelim (H (refl_eq …))
884 nlemma neq_to_neqquintuple :
886 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
887 (∀x,y:T1.decidable (x = y)) →
888 (∀x,y:T2.decidable (x = y)) →
889 (∀x,y:T3.decidable (x = y)) →
890 (∀x,y:T4.decidable (x = y)) →
891 (∀x,y:T5.decidable (x = y)) →
892 (∀x,y:T1.x ≠ y → f1 x y = false) →
893 (∀x,y:T2.x ≠ y → f2 x y = false) →
894 (∀x,y:T3.x ≠ y → f3 x y = false) →
895 (∀x,y:T4.x ≠ y → f4 x y = false) →
896 (∀x,y:T5.x ≠ y → f5 x y = false) →
897 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
898 (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false)).
899 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5;
900 #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
901 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
902 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
903 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
904 napply (or5_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2) ? (quintuple_destruct T1 T2 T3 T4 T5 H1 H2 H3 H4 H5 … H) ?);
905 ##[ ##1: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
906 ##| ##2: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
907 ##| ##3: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
908 ##| ##4: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
909 ##| ##5: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq