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 (* This file was automatically generated: do not edit *********************)
17 include "LambdaDelta-1/csubst0/defs.ma".
19 theorem csubst0_gen_sort:
20 \forall (x: C).(\forall (v: T).(\forall (i: nat).(\forall (n: nat).((csubst0
21 i v (CSort n) x) \to (\forall (P: Prop).P)))))
23 \lambda (x: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda
24 (H: (csubst0 i v (CSort n) x)).(\lambda (P: Prop).(let H0 \def (match H in
25 csubst0 return (\lambda (n0: nat).(\lambda (t: T).(\lambda (c: C).(\lambda
26 (c0: C).(\lambda (_: (csubst0 n0 t c c0)).((eq nat n0 i) \to ((eq T t v) \to
27 ((eq C c (CSort n)) \to ((eq C c0 x) \to P))))))))) with [(csubst0_snd k i0
28 v0 u1 u2 H0 c) \Rightarrow (\lambda (H1: (eq nat (s k i0) i)).(\lambda (H2:
29 (eq T v0 v)).(\lambda (H3: (eq C (CHead c k u1) (CSort n))).(\lambda (H4: (eq
30 C (CHead c k u2) x)).(eq_ind nat (s k i0) (\lambda (_: nat).((eq T v0 v) \to
31 ((eq C (CHead c k u1) (CSort n)) \to ((eq C (CHead c k u2) x) \to ((subst0 i0
32 v0 u1 u2) \to P))))) (\lambda (H5: (eq T v0 v)).(eq_ind T v (\lambda (t:
33 T).((eq C (CHead c k u1) (CSort n)) \to ((eq C (CHead c k u2) x) \to ((subst0
34 i0 t u1 u2) \to P)))) (\lambda (H6: (eq C (CHead c k u1) (CSort n))).(let H7
35 \def (eq_ind C (CHead c k u1) (\lambda (e: C).(match e in C return (\lambda
36 (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow
37 True])) I (CSort n) H6) in (False_ind ((eq C (CHead c k u2) x) \to ((subst0
38 i0 v u1 u2) \to P)) H7))) v0 (sym_eq T v0 v H5))) i H1 H2 H3 H4 H0))))) |
39 (csubst0_fst k i0 c1 c2 v0 H0 u) \Rightarrow (\lambda (H1: (eq nat (s k i0)
40 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq C (CHead c1 k u) (CSort
41 n))).(\lambda (H4: (eq C (CHead c2 k u) x)).(eq_ind nat (s k i0) (\lambda (_:
42 nat).((eq T v0 v) \to ((eq C (CHead c1 k u) (CSort n)) \to ((eq C (CHead c2 k
43 u) x) \to ((csubst0 i0 v0 c1 c2) \to P))))) (\lambda (H5: (eq T v0
44 v)).(eq_ind T v (\lambda (t: T).((eq C (CHead c1 k u) (CSort n)) \to ((eq C
45 (CHead c2 k u) x) \to ((csubst0 i0 t c1 c2) \to P)))) (\lambda (H6: (eq C
46 (CHead c1 k u) (CSort n))).(let H7 \def (eq_ind C (CHead c1 k u) (\lambda (e:
47 C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
48 False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H6) in (False_ind ((eq
49 C (CHead c2 k u) x) \to ((csubst0 i0 v c1 c2) \to P)) H7))) v0 (sym_eq T v0 v
50 H5))) i H1 H2 H3 H4 H0))))) | (csubst0_both k i0 v0 u1 u2 H0 c1 c2 H1)
51 \Rightarrow (\lambda (H2: (eq nat (s k i0) i)).(\lambda (H3: (eq T v0
52 v)).(\lambda (H4: (eq C (CHead c1 k u1) (CSort n))).(\lambda (H5: (eq C
53 (CHead c2 k u2) x)).(eq_ind nat (s k i0) (\lambda (_: nat).((eq T v0 v) \to
54 ((eq C (CHead c1 k u1) (CSort n)) \to ((eq C (CHead c2 k u2) x) \to ((subst0
55 i0 v0 u1 u2) \to ((csubst0 i0 v0 c1 c2) \to P)))))) (\lambda (H6: (eq T v0
56 v)).(eq_ind T v (\lambda (t: T).((eq C (CHead c1 k u1) (CSort n)) \to ((eq C
57 (CHead c2 k u2) x) \to ((subst0 i0 t u1 u2) \to ((csubst0 i0 t c1 c2) \to
58 P))))) (\lambda (H7: (eq C (CHead c1 k u1) (CSort n))).(let H8 \def (eq_ind C
59 (CHead c1 k u1) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop)
60 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
61 (CSort n) H7) in (False_ind ((eq C (CHead c2 k u2) x) \to ((subst0 i0 v u1
62 u2) \to ((csubst0 i0 v c1 c2) \to P))) H8))) v0 (sym_eq T v0 v H6))) i H2 H3
63 H4 H5 H0 H1)))))]) in (H0 (refl_equal nat i) (refl_equal T v) (refl_equal C
64 (CSort n)) (refl_equal C x)))))))).
66 theorem csubst0_gen_head:
67 \forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall
68 (v: T).(\forall (i: nat).((csubst0 i v (CHead c1 k u1) x) \to (or3 (ex3_2 T
69 nat (\lambda (_: T).(\lambda (j: nat).(eq nat i (s k j)))) (\lambda (u2:
70 T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
71 nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
72 nat i (s k j)))) (\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2 k
73 u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C
74 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat i (s k j)))))
75 (\lambda (u2: T).(\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2 k
76 u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
77 u2)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
80 \lambda (k: K).(\lambda (c1: C).(\lambda (x: C).(\lambda (u1: T).(\lambda
81 (v: T).(\lambda (i: nat).(\lambda (H: (csubst0 i v (CHead c1 k u1) x)).(let
82 H0 \def (match H in csubst0 return (\lambda (n: nat).(\lambda (t: T).(\lambda
83 (c: C).(\lambda (c0: C).(\lambda (_: (csubst0 n t c c0)).((eq nat n i) \to
84 ((eq T t v) \to ((eq C c (CHead c1 k u1)) \to ((eq C c0 x) \to (or3 (ex3_2 T
85 nat (\lambda (_: T).(\lambda (j: nat).(eq nat i (s k j)))) (\lambda (u2:
86 T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
87 nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
88 nat i (s k j)))) (\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2 k
89 u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C
90 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat i (s k j)))))
91 (\lambda (u2: T).(\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2 k
92 u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
93 u2)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
94 c2))))))))))))))) with [(csubst0_snd k0 i0 v0 u0 u2 H0 c) \Rightarrow
95 (\lambda (H1: (eq nat (s k0 i0) i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3:
96 (eq C (CHead c k0 u0) (CHead c1 k u1))).(\lambda (H4: (eq C (CHead c k0 u2)
97 x)).(eq_ind nat (s k0 i0) (\lambda (n: nat).((eq T v0 v) \to ((eq C (CHead c
98 k0 u0) (CHead c1 k u1)) \to ((eq C (CHead c k0 u2) x) \to ((subst0 i0 v0 u0
99 u2) \to (or3 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat n (s k
100 j)))) (\lambda (u3: T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda
101 (u3: T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_:
102 C).(\lambda (j: nat).(eq nat n (s k j)))) (\lambda (c2: C).(\lambda (_:
103 nat).(eq C x (CHead c2 k u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j
104 v c1 c2)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
105 nat).(eq nat n (s k j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_:
106 nat).(eq C x (CHead c2 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda
107 (j: nat).(subst0 j v u1 u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j:
108 nat).(csubst0 j v c1 c2))))))))))) (\lambda (H5: (eq T v0 v)).(eq_ind T v
109 (\lambda (t: T).((eq C (CHead c k0 u0) (CHead c1 k u1)) \to ((eq C (CHead c
110 k0 u2) x) \to ((subst0 i0 t u0 u2) \to (or3 (ex3_2 T nat (\lambda (_:
111 T).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (u3: T).(\lambda
112 (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
113 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
114 nat (s k0 i0) (s k j)))) (\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2
115 k u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C
116 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k0 i0) (s k
117 j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2
118 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
119 u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
120 c2)))))))))) (\lambda (H6: (eq C (CHead c k0 u0) (CHead c1 k u1))).(let H7
121 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
122 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c k0
123 u0) (CHead c1 k u1) H6) in ((let H8 \def (f_equal C K (\lambda (e: C).(match
124 e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1
125 _) \Rightarrow k1])) (CHead c k0 u0) (CHead c1 k u1) H6) in ((let H9 \def
126 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
127 [(CSort _) \Rightarrow c | (CHead c0 _ _) \Rightarrow c0])) (CHead c k0 u0)
128 (CHead c1 k u1) H6) in (eq_ind C c1 (\lambda (c0: C).((eq K k0 k) \to ((eq T
129 u0 u1) \to ((eq C (CHead c0 k0 u2) x) \to ((subst0 i0 v u0 u2) \to (or3
130 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k0 i0) (s k j))))
131 (\lambda (u3: T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3:
132 T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_:
133 C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (c2: C).(\lambda
134 (_: nat).(eq C x (CHead c2 k u1)))) (\lambda (c2: C).(\lambda (j:
135 nat).(csubst0 j v c1 c2)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
136 C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j))))) (\lambda (u3: T).(\lambda
137 (c2: C).(\lambda (_: nat).(eq C x (CHead c2 k u3))))) (\lambda (u3:
138 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_:
139 T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2))))))))))) (\lambda
140 (H10: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T u0 u1) \to ((eq C
141 (CHead c1 k1 u2) x) \to ((subst0 i0 v u0 u2) \to (or3 (ex3_2 T nat (\lambda
142 (_: T).(\lambda (j: nat).(eq nat (s k1 i0) (s k j)))) (\lambda (u3:
143 T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
144 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
145 nat (s k1 i0) (s k j)))) (\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2
146 k u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C
147 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k1 i0) (s k
148 j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2
149 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
150 u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
151 c2)))))))))) (\lambda (H11: (eq T u0 u1)).(eq_ind T u1 (\lambda (t: T).((eq C
152 (CHead c1 k u2) x) \to ((subst0 i0 v t u2) \to (or3 (ex3_2 T nat (\lambda (_:
153 T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u3: T).(\lambda
154 (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
155 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
156 nat (s k i0) (s k j)))) (\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2
157 k u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C
158 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
159 j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_: nat).(eq C x (CHead c2
160 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
161 u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
162 c2))))))))) (\lambda (H12: (eq C (CHead c1 k u2) x)).(eq_ind C (CHead c1 k
163 u2) (\lambda (c0: C).((subst0 i0 v u1 u2) \to (or3 (ex3_2 T nat (\lambda (_:
164 T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u3: T).(\lambda
165 (_: nat).(eq C c0 (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
166 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
167 nat (s k i0) (s k j)))) (\lambda (c2: C).(\lambda (_: nat).(eq C c0 (CHead c2
168 k u1)))) (\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C
169 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
170 j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_: nat).(eq C c0 (CHead c2
171 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
172 u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
173 c2)))))))) (\lambda (H13: (subst0 i0 v u1 u2)).(let H14 \def (eq_ind K k0
174 (\lambda (k1: K).(eq nat (s k1 i0) i)) H1 k H10) in (or3_intro0 (ex3_2 T nat
175 (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u3:
176 T).(\lambda (_: nat).(eq C (CHead c1 k u2) (CHead c1 k u3)))) (\lambda (u3:
177 T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_:
178 C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (c2: C).(\lambda
179 (_: nat).(eq C (CHead c1 k u2) (CHead c2 k u1)))) (\lambda (c2: C).(\lambda
180 (j: nat).(csubst0 j v c1 c2)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
181 C).(\lambda (j: nat).(eq nat (s k i0) (s k j))))) (\lambda (u3: T).(\lambda
182 (c2: C).(\lambda (_: nat).(eq C (CHead c1 k u2) (CHead c2 k u3))))) (\lambda
183 (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_:
184 T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1 c2))))) (ex3_2_intro T
185 nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda
186 (u3: T).(\lambda (_: nat).(eq C (CHead c1 k u2) (CHead c1 k u3)))) (\lambda
187 (u3: T).(\lambda (j: nat).(subst0 j v u1 u3))) u2 i0 (refl_equal nat (s k
188 i0)) (refl_equal C (CHead c1 k u2)) H13)))) x H12)) u0 (sym_eq T u0 u1 H11)))
189 k0 (sym_eq K k0 k H10))) c (sym_eq C c c1 H9))) H8)) H7))) v0 (sym_eq T v0 v
190 H5))) i H1 H2 H3 H4 H0))))) | (csubst0_fst k0 i0 c0 c2 v0 H0 u) \Rightarrow
191 (\lambda (H1: (eq nat (s k0 i0) i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3:
192 (eq C (CHead c0 k0 u) (CHead c1 k u1))).(\lambda (H4: (eq C (CHead c2 k0 u)
193 x)).(eq_ind nat (s k0 i0) (\lambda (n: nat).((eq T v0 v) \to ((eq C (CHead c0
194 k0 u) (CHead c1 k u1)) \to ((eq C (CHead c2 k0 u) x) \to ((csubst0 i0 v0 c0
195 c2) \to (or3 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat n (s k
196 j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda
197 (u2: T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_:
198 C).(\lambda (j: nat).(eq nat n (s k j)))) (\lambda (c3: C).(\lambda (_:
199 nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j
200 v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
201 nat).(eq nat n (s k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_:
202 nat).(eq C x (CHead c3 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda
203 (j: nat).(subst0 j v u1 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j:
204 nat).(csubst0 j v c1 c3))))))))))) (\lambda (H5: (eq T v0 v)).(eq_ind T v
205 (\lambda (t: T).((eq C (CHead c0 k0 u) (CHead c1 k u1)) \to ((eq C (CHead c2
206 k0 u) x) \to ((csubst0 i0 t c0 c2) \to (or3 (ex3_2 T nat (\lambda (_:
207 T).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (u2: T).(\lambda
208 (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
209 nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
210 nat (s k0 i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
211 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
212 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k0 i0) (s k
213 j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
214 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
215 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
216 c3)))))))))) (\lambda (H6: (eq C (CHead c0 k0 u) (CHead c1 k u1))).(let H7
217 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
218 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0
219 u) (CHead c1 k u1) H6) in ((let H8 \def (f_equal C K (\lambda (e: C).(match e
220 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1
221 _) \Rightarrow k1])) (CHead c0 k0 u) (CHead c1 k u1) H6) in ((let H9 \def
222 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
223 [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k0 u)
224 (CHead c1 k u1) H6) in (eq_ind C c1 (\lambda (c: C).((eq K k0 k) \to ((eq T u
225 u1) \to ((eq C (CHead c2 k0 u) x) \to ((csubst0 i0 v c c2) \to (or3 (ex3_2 T
226 nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda
227 (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2:
228 T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_:
229 C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (c3: C).(\lambda
230 (_: nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j:
231 nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
232 C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j))))) (\lambda (u2: T).(\lambda
233 (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u2))))) (\lambda (u2:
234 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
235 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))))))))) (\lambda
236 (H10: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T u u1) \to ((eq C
237 (CHead c2 k1 u) x) \to ((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat (\lambda
238 (_: T).(\lambda (j: nat).(eq nat (s k1 i0) (s k j)))) (\lambda (u2:
239 T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
240 nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
241 nat (s k1 i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
242 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
243 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k1 i0) (s k
244 j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
245 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
246 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
247 c3)))))))))) (\lambda (H11: (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((eq C
248 (CHead c2 k t) x) \to ((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat (\lambda
249 (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u2:
250 T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
251 nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
252 nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
253 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
254 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
255 j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
256 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
257 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
258 c3))))))))) (\lambda (H12: (eq C (CHead c2 k u1) x)).(eq_ind C (CHead c2 k
259 u1) (\lambda (c: C).((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat (\lambda (_:
260 T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u2: T).(\lambda
261 (_: nat).(eq C c (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
262 nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
263 nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C c (CHead c3
264 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
265 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
266 j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C c (CHead c3
267 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
268 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
269 c3)))))))) (\lambda (H13: (csubst0 i0 v c1 c2)).(let H14 \def (eq_ind K k0
270 (\lambda (k1: K).(eq nat (s k1 i0) i)) H1 k H10) in (or3_intro1 (ex3_2 T nat
271 (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u2:
272 T).(\lambda (_: nat).(eq C (CHead c2 k u1) (CHead c1 k u2)))) (\lambda (u2:
273 T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_:
274 C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda
275 (_: nat).(eq C (CHead c2 k u1) (CHead c3 k u1)))) (\lambda (c3: C).(\lambda
276 (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
277 C).(\lambda (j: nat).(eq nat (s k i0) (s k j))))) (\lambda (u2: T).(\lambda
278 (c3: C).(\lambda (_: nat).(eq C (CHead c2 k u1) (CHead c3 k u2))))) (\lambda
279 (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
280 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2_intro C
281 nat (\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda
282 (c3: C).(\lambda (_: nat).(eq C (CHead c2 k u1) (CHead c3 k u1)))) (\lambda
283 (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))) c2 i0 (refl_equal nat (s k
284 i0)) (refl_equal C (CHead c2 k u1)) H13)))) x H12)) u (sym_eq T u u1 H11)))
285 k0 (sym_eq K k0 k H10))) c0 (sym_eq C c0 c1 H9))) H8)) H7))) v0 (sym_eq T v0
286 v H5))) i H1 H2 H3 H4 H0))))) | (csubst0_both k0 i0 v0 u0 u2 H0 c0 c2 H1)
287 \Rightarrow (\lambda (H2: (eq nat (s k0 i0) i)).(\lambda (H3: (eq T v0
288 v)).(\lambda (H4: (eq C (CHead c0 k0 u0) (CHead c1 k u1))).(\lambda (H5: (eq
289 C (CHead c2 k0 u2) x)).(eq_ind nat (s k0 i0) (\lambda (n: nat).((eq T v0 v)
290 \to ((eq C (CHead c0 k0 u0) (CHead c1 k u1)) \to ((eq C (CHead c2 k0 u2) x)
291 \to ((subst0 i0 v0 u0 u2) \to ((csubst0 i0 v0 c0 c2) \to (or3 (ex3_2 T nat
292 (\lambda (_: T).(\lambda (j: nat).(eq nat n (s k j)))) (\lambda (u3:
293 T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
294 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
295 nat n (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k
296 u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
297 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat n (s k j)))))
298 (\lambda (u3: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k
299 u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
300 u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
301 c3)))))))))))) (\lambda (H6: (eq T v0 v)).(eq_ind T v (\lambda (t: T).((eq C
302 (CHead c0 k0 u0) (CHead c1 k u1)) \to ((eq C (CHead c2 k0 u2) x) \to ((subst0
303 i0 t u0 u2) \to ((csubst0 i0 t c0 c2) \to (or3 (ex3_2 T nat (\lambda (_:
304 T).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (u3: T).(\lambda
305 (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
306 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
307 nat (s k0 i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
308 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
309 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k0 i0) (s k
310 j))))) (\lambda (u3: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
311 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
312 u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
313 c3))))))))))) (\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c1 k u1))).(let H8
314 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
315 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0
316 u0) (CHead c1 k u1) H7) in ((let H9 \def (f_equal C K (\lambda (e: C).(match
317 e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1
318 _) \Rightarrow k1])) (CHead c0 k0 u0) (CHead c1 k u1) H7) in ((let H10 \def
319 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
320 [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k0 u0)
321 (CHead c1 k u1) H7) in (eq_ind C c1 (\lambda (c: C).((eq K k0 k) \to ((eq T
322 u0 u1) \to ((eq C (CHead c2 k0 u2) x) \to ((subst0 i0 v u0 u2) \to ((csubst0
323 i0 v c c2) \to (or3 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s
324 k0 i0) (s k j)))) (\lambda (u3: T).(\lambda (_: nat).(eq C x (CHead c1 k
325 u3)))) (\lambda (u3: T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat
326 (\lambda (_: C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (c3:
327 C).(\lambda (_: nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j:
328 nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
329 C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j))))) (\lambda (u3: T).(\lambda
330 (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u3))))) (\lambda (u3:
331 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_:
332 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))))))))))) (\lambda
333 (H11: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T u0 u1) \to ((eq C
334 (CHead c2 k1 u2) x) \to ((subst0 i0 v u0 u2) \to ((csubst0 i0 v c1 c2) \to
335 (or3 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k1 i0) (s k
336 j)))) (\lambda (u3: T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda
337 (u3: T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_:
338 C).(\lambda (j: nat).(eq nat (s k1 i0) (s k j)))) (\lambda (c3: C).(\lambda
339 (_: nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j:
340 nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
341 C).(\lambda (j: nat).(eq nat (s k1 i0) (s k j))))) (\lambda (u3: T).(\lambda
342 (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u3))))) (\lambda (u3:
343 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_:
344 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))))))))) (\lambda
345 (H12: (eq T u0 u1)).(eq_ind T u1 (\lambda (t: T).((eq C (CHead c2 k u2) x)
346 \to ((subst0 i0 v t u2) \to ((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat
347 (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u3:
348 T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
349 nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
350 nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
351 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
352 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
353 j))))) (\lambda (u3: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
354 k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
355 u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
356 c3)))))))))) (\lambda (H13: (eq C (CHead c2 k u2) x)).(eq_ind C (CHead c2 k
357 u2) (\lambda (c: C).((subst0 i0 v u1 u2) \to ((csubst0 i0 v c1 c2) \to (or3
358 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j))))
359 (\lambda (u3: T).(\lambda (_: nat).(eq C c (CHead c1 k u3)))) (\lambda (u3:
360 T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_:
361 C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda
362 (_: nat).(eq C c (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j:
363 nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
364 C).(\lambda (j: nat).(eq nat (s k i0) (s k j))))) (\lambda (u3: T).(\lambda
365 (c3: C).(\lambda (_: nat).(eq C c (CHead c3 k u3))))) (\lambda (u3:
366 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_:
367 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))))))) (\lambda
368 (H14: (subst0 i0 v u1 u2)).(\lambda (H15: (csubst0 i0 v c1 c2)).(let H16 \def
369 (eq_ind K k0 (\lambda (k1: K).(eq nat (s k1 i0) i)) H2 k H11) in (or3_intro2
370 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j))))
371 (\lambda (u3: T).(\lambda (_: nat).(eq C (CHead c2 k u2) (CHead c1 k u3))))
372 (\lambda (u3: T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat
373 (\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (c3:
374 C).(\lambda (_: nat).(eq C (CHead c2 k u2) (CHead c3 k u1)))) (\lambda (c3:
375 C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_:
376 T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k j))))) (\lambda
377 (u3: T).(\lambda (c3: C).(\lambda (_: nat).(eq C (CHead c2 k u2) (CHead c3 k
378 u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
379 u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
380 c3))))) (ex4_3_intro T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
381 nat).(eq nat (s k i0) (s k j))))) (\lambda (u3: T).(\lambda (c3: C).(\lambda
382 (_: nat).(eq C (CHead c2 k u2) (CHead c3 k u3))))) (\lambda (u3: T).(\lambda
383 (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_: T).(\lambda (c3:
384 C).(\lambda (j: nat).(csubst0 j v c1 c3)))) u2 c2 i0 (refl_equal nat (s k
385 i0)) (refl_equal C (CHead c2 k u2)) H14 H15))))) x H13)) u0 (sym_eq T u0 u1
386 H12))) k0 (sym_eq K k0 k H11))) c0 (sym_eq C c0 c1 H10))) H9)) H8))) v0
387 (sym_eq T v0 v H6))) i H2 H3 H4 H5 H0 H1)))))]) in (H0 (refl_equal nat i)
388 (refl_equal T v) (refl_equal C (CHead c1 k u1)) (refl_equal C x))))))))).
projects / helm.git / blob