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.
48 ∀T1:∀x0:T0. a0=x0 → Type[0].
49 ∀a1:T1 a0 (refl ? a0).
50 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
54 ∀e1:R1 ??? a1 ? e0 = b1.
55 ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
56 #T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
57 napply (eq_rect_Type0 ????? e1);
58 napply (R1 ?? ? ?? e0);
65 ∀T1:∀x0:T0. a0=x0 → Type[0].
66 ∀a1:T1 a0 (refl ? a0).
67 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
68 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
69 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
70 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 x0 p0 ? p1 a2 = x2 → Type[0].
74 ∀e1:R1 ??? a1 ? e0 = b1.
76 ∀e2:R2 ???? T2 b0 e0 ? e1 a2 = b2.
77 ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
78 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
79 napply (eq_rect_Type0 ????? e2);
80 napply (R2 ?? ? ??? e0 ? e1);