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 (**************************************************************************)
16 include "list/list.ma".
18 inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
19 | il_s : ∀n.T n → index_list T n n
20 | il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
22 lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
23 ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
25 [destruct;apply il_s;apply f;assumption
27 [apply f;rewrite > H;assumption
29 [rewrite > H;reflexivity
33 definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
34 λT0:Type.λT1:T0 → Type.
38 eq_rect' ?? (λy,p.T1 y) so ? e0.
41 include "logic/equality.ma".
43 ndefinition R1 ≝ eq_rect_Type0.
47 ∀T1:∀x0:T0. a0=x0 → Type[0].
48 ∀a1:T1 a0 (refl ? a0).
49 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
53 ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
54 ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
55 #T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
56 napply (eq_rect_Type0 ????? e1);
57 napply (R1 ?? ? ?? e0);
64 ∀T1:∀x0:T0. a0=x0 → Type[0].
65 ∀a1:T1 a0 (refl ? a0).
66 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
67 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
68 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
69 ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
73 ∀e1:R1 ? a0 ? a1 ? e0 = b1.
75 ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
76 ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
77 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
78 napply (eq_rect_Type0 ????? e2);
79 napply (R2 ?? ? ??? e0 ? e1);