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 "basic_1A/pr3/defs.ma".
19 include "basic_1A/pr2/fwd.ma".
21 implied rec lemma pr3_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall (t:
22 T).(P t t))) (f0: (\forall (t2: T).(\forall (t1: T).((pr2 c t1 t2) \to
23 (\forall (t3: T).((pr3 c t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (t: T)
24 (t0: T) (p: pr3 c t t0) on p: P t t0 \def match p with [(pr3_refl t1)
25 \Rightarrow (f t1) | (pr3_sing t2 t1 p0 t3 p1) \Rightarrow (f0 t2 t1 p0 t3 p1
26 ((pr3_ind c P f f0) t2 t3 p1))].
29 \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TSort n) x) \to
32 \lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr3 c (TSort
33 n) x)).(insert_eq T (TSort n) (\lambda (t: T).(pr3 c t x)) (\lambda (t:
34 T).(eq T x t)) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(pr3_ind c (\lambda
35 (t: T).(\lambda (t0: T).((eq T t (TSort n)) \to (eq T t0 t)))) (\lambda (t:
36 T).(\lambda (_: (eq T t (TSort n))).(refl_equal T t))) (\lambda (t2:
37 T).(\lambda (t1: T).(\lambda (H1: (pr2 c t1 t2)).(\lambda (t3: T).(\lambda
38 (_: (pr3 c t2 t3)).(\lambda (H3: (((eq T t2 (TSort n)) \to (eq T t3
39 t2)))).(\lambda (H4: (eq T t1 (TSort n))).(let H5 \def (eq_ind T t1 (\lambda
40 (t: T).(pr2 c t t2)) H1 (TSort n) H4) in (eq_ind_r T (TSort n) (\lambda (t:
41 T).(eq T t3 t)) (let H6 \def (eq_ind T t2 (\lambda (t: T).((eq T t (TSort n))
42 \to (eq T t3 t))) H3 (TSort n) (pr2_gen_sort c t2 n H5)) in (H6 (refl_equal T
43 (TSort n)))) t1 H4))))))))) y x H0))) H)))).
46 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
47 (THead (Bind Abst) u1 t1) x) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
48 T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
49 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u:
50 T).(pr3 (CHead c (Bind b) u) t1 t2))))))))))
52 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
53 (H: (pr3 c (THead (Bind Abst) u1 t1) x)).(insert_eq T (THead (Bind Abst) u1
54 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(ex3_2 T T (\lambda (u2:
55 T).(\lambda (t2: T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2:
56 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
57 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t2))))))) (\lambda (y:
58 T).(\lambda (H0: (pr3 c y x)).(unintro T t1 (\lambda (t: T).((eq T y (THead
59 (Bind Abst) u1 t)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x
60 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
61 (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
62 c (Bind b) u) t t2)))))))) (unintro T u1 (\lambda (t: T).(\forall (x0:
63 T).((eq T y (THead (Bind Abst) t x0)) \to (ex3_2 T T (\lambda (u2:
64 T).(\lambda (t2: T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2:
65 T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
66 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x0 t2))))))))) (pr3_ind c
67 (\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).(\forall (x1: T).((eq T t
68 (THead (Bind Abst) x0 x1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
69 T).(eq T t0 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
70 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
71 (u: T).(pr3 (CHead c (Bind b) u) x1 t2))))))))))) (\lambda (t: T).(\lambda
72 (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T t (THead (Bind Abst) x0
73 x1))).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T t (THead (Bind
74 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
75 T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
76 x1 t2))))) x0 x1 H1 (pr3_refl c x0) (\lambda (b: B).(\lambda (u: T).(pr3_refl
77 (CHead c (Bind b) u) x1)))))))) (\lambda (t2: T).(\lambda (t3: T).(\lambda
78 (H1: (pr2 c t3 t2)).(\lambda (t4: T).(\lambda (_: (pr3 c t2 t4)).(\lambda
79 (H3: ((\forall (x0: T).(\forall (x1: T).((eq T t2 (THead (Bind Abst) x0 x1))
80 \to (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst)
81 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
82 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
83 x1 t5))))))))))).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t3
84 (THead (Bind Abst) x0 x1))).(let H5 \def (eq_ind T t3 (\lambda (t: T).(pr2 c
85 t t2)) H1 (THead (Bind Abst) x0 x1) H4) in (let H6 \def (pr2_gen_abst c x0 x1
86 t2 H5) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead
87 (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
88 (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead
89 c (Bind b) u) x1 t5))))) (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
90 t4 (THead (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
91 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
92 (CHead c (Bind b) u) x1 t5)))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda
93 (H7: (eq T t2 (THead (Bind Abst) x2 x3))).(\lambda (H8: (pr2 c x0
94 x2)).(\lambda (H9: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
95 x1 x3))))).(let H10 \def (eq_ind T t2 (\lambda (t: T).(\forall (x4:
96 T).(\forall (x5: T).((eq T t (THead (Bind Abst) x4 x5)) \to (ex3_2 T T
97 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5))))
98 (\lambda (u2: T).(\lambda (_: T).(pr3 c x4 u2))) (\lambda (_: T).(\lambda
99 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x5
100 t5)))))))))) H3 (THead (Bind Abst) x2 x3) H7) in (let H11 \def (H10 x2 x3
101 (refl_equal T (THead (Bind Abst) x2 x3))) in (ex3_2_ind T T (\lambda (u2:
102 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5)))) (\lambda (u2:
103 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
104 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 t5))))) (ex3_2 T T
105 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5))))
106 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
107 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5))))))
108 (\lambda (x4: T).(\lambda (x5: T).(\lambda (H12: (eq T t4 (THead (Bind Abst)
109 x4 x5))).(\lambda (H13: (pr3 c x2 x4)).(\lambda (H14: ((\forall (b:
110 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 x5))))).(ex3_2_intro T T
111 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5))))
112 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
113 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5)))))
114 x4 x5 H12 (pr3_sing c x2 x0 H8 x4 H13) (\lambda (b: B).(\lambda (u:
115 T).(pr3_sing (CHead c (Bind b) u) x3 x1 (H9 b u) x5 (H14 b u))))))))))
116 H11)))))))) H6)))))))))))) y x H0))))) H))))).
119 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
120 (THead (Flat Cast) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
121 (t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_:
122 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c t1 t2)))) (pr3 c
125 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
126 (H: (pr3 c (THead (Flat Cast) u1 t1) x)).(insert_eq T (THead (Flat Cast) u1
127 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2:
128 T).(\lambda (t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2:
129 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c t1
130 t2)))) (pr3 c t1 x))) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(unintro T
131 t1 (\lambda (t: T).((eq T y (THead (Flat Cast) u1 t)) \to (or (ex3_2 T T
132 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Flat Cast) u2 t2))))
133 (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda
134 (t2: T).(pr3 c t t2)))) (pr3 c t x)))) (unintro T u1 (\lambda (t: T).(\forall
135 (x0: T).((eq T y (THead (Flat Cast) t x0)) \to (or (ex3_2 T T (\lambda (u2:
136 T).(\lambda (t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2:
137 T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c x0
138 t2)))) (pr3 c x0 x))))) (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall
139 (x0: T).(\forall (x1: T).((eq T t (THead (Flat Cast) x0 x1)) \to (or (ex3_2 T
140 T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) u2 t2))))
141 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
142 (t2: T).(pr3 c x1 t2)))) (pr3 c x1 t0))))))) (\lambda (t: T).(\lambda (x0:
143 T).(\lambda (x1: T).(\lambda (H1: (eq T t (THead (Flat Cast) x0
144 x1))).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t0: T).(or (ex3_2 T T
145 (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) u2 t2))))
146 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
147 (t2: T).(pr3 c x1 t2)))) (pr3 c x1 t0))) (or_introl (ex3_2 T T (\lambda (u2:
148 T).(\lambda (t2: T).(eq T (THead (Flat Cast) x0 x1) (THead (Flat Cast) u2
149 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
150 T).(\lambda (t2: T).(pr3 c x1 t2)))) (pr3 c x1 (THead (Flat Cast) x0 x1))
151 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Cast)
152 x0 x1) (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c
153 x0 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c x1 t2))) x0 x1 (refl_equal T
154 (THead (Flat Cast) x0 x1)) (pr3_refl c x0) (pr3_refl c x1))) t H1)))))
155 (\lambda (t2: T).(\lambda (t3: T).(\lambda (H1: (pr2 c t3 t2)).(\lambda (t4:
156 T).(\lambda (H2: (pr3 c t2 t4)).(\lambda (H3: ((\forall (x0: T).(\forall (x1:
157 T).((eq T t2 (THead (Flat Cast) x0 x1)) \to (or (ex3_2 T T (\lambda (u2:
158 T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
159 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1
160 t5)))) (pr3 c x1 t4))))))).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H4:
161 (eq T t3 (THead (Flat Cast) x0 x1))).(let H5 \def (eq_ind T t3 (\lambda (t:
162 T).(pr2 c t t2)) H1 (THead (Flat Cast) x0 x1) H4) in (let H6 \def
163 (pr2_gen_cast c x0 x1 t2 H5) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
164 (t5: T).(eq T t2 (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
165 T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr2 c x1 t5)))) (pr2 c
166 x1 t2) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
167 Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
168 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4)) (\lambda (H7: (ex3_2 T T
169 (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Flat Cast) u2 t5))))
170 (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda
171 (t5: T).(pr2 c x1 t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5:
172 T).(eq T t2 (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
173 T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr2 c x1 t5))) (or
174 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2
175 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
176 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4)) (\lambda (x2: T).(\lambda
177 (x3: T).(\lambda (H8: (eq T t2 (THead (Flat Cast) x2 x3))).(\lambda (H9: (pr2
178 c x0 x2)).(\lambda (H10: (pr2 c x1 x3)).(let H11 \def (eq_ind T t2 (\lambda
179 (t: T).(\forall (x4: T).(\forall (x5: T).((eq T t (THead (Flat Cast) x4 x5))
180 \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
181 Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x4 u2))) (\lambda (_:
182 T).(\lambda (t5: T).(pr3 c x5 t5)))) (pr3 c x5 t4)))))) H3 (THead (Flat Cast)
183 x2 x3) H8) in (let H12 \def (H11 x2 x3 (refl_equal T (THead (Flat Cast) x2
184 x3))) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
185 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))
186 (\lambda (_: T).(\lambda (t5: T).(pr3 c x3 t5)))) (pr3 c x3 t4) (or (ex3_2 T
187 T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5))))
188 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
189 (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4)) (\lambda (H13: (ex3_2 T T (\lambda
190 (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
191 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x3
192 t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
193 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))
194 (\lambda (_: T).(\lambda (t5: T).(pr3 c x3 t5))) (or (ex3_2 T T (\lambda (u2:
195 T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
196 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1
197 t5)))) (pr3 c x1 t4)) (\lambda (x4: T).(\lambda (x5: T).(\lambda (H14: (eq T
198 t4 (THead (Flat Cast) x4 x5))).(\lambda (H15: (pr3 c x2 x4)).(\lambda (H16:
199 (pr3 c x3 x5)).(eq_ind_r T (THead (Flat Cast) x4 x5) (\lambda (t: T).(or
200 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t (THead (Flat Cast) u2
201 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
202 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t))) (or_introl (ex3_2 T T
203 (\lambda (u2: T).(\lambda (t5: T).(eq T (THead (Flat Cast) x4 x5) (THead
204 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
205 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 (THead (Flat
206 Cast) x4 x5)) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t5: T).(eq T (THead
207 (Flat Cast) x4 x5) (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
208 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5))) x4 x5
209 (refl_equal T (THead (Flat Cast) x4 x5)) (pr3_sing c x2 x0 H9 x4 H15)
210 (pr3_sing c x3 x1 H10 x5 H16))) t4 H14)))))) H13)) (\lambda (H13: (pr3 c x3
211 t4)).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
212 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
213 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4) (pr3_sing c
214 x3 x1 H10 t4 H13))) H12)))))))) H7)) (\lambda (H7: (pr2 c x1 t2)).(or_intror
215 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2
216 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
217 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4) (pr3_sing c t2 x1 H7 t4
218 H2))) H6)))))))))))) y x H0))))) H))))).
221 \forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall
222 (d: nat).((pr3 c (lift h d t1) x) \to (\forall (e: C).((drop h d c e) \to
223 (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr3 e t1
226 \lambda (c: C).(\lambda (t1: T).(\lambda (x: T).(\lambda (h: nat).(\lambda
227 (d: nat).(\lambda (H: (pr3 c (lift h d t1) x)).(insert_eq T (lift h d t1)
228 (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(\forall (e: C).((drop h d c e)
229 \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr3 e
230 t1 t2)))))) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(unintro T t1 (\lambda
231 (t: T).((eq T y (lift h d t)) \to (\forall (e: C).((drop h d c e) \to (ex2 T
232 (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr3 e t t2)))))))
233 (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).((eq T t (lift h
234 d x0)) \to (\forall (e: C).((drop h d c e) \to (ex2 T (\lambda (t2: T).(eq T
235 t0 (lift h d t2))) (\lambda (t2: T).(pr3 e x0 t2))))))))) (\lambda (t:
236 T).(\lambda (x0: T).(\lambda (H1: (eq T t (lift h d x0))).(\lambda (e:
237 C).(\lambda (_: (drop h d c e)).(ex_intro2 T (\lambda (t2: T).(eq T t (lift h
238 d t2))) (\lambda (t2: T).(pr3 e x0 t2)) x0 H1 (pr3_refl e x0))))))) (\lambda
239 (t2: T).(\lambda (t3: T).(\lambda (H1: (pr2 c t3 t2)).(\lambda (t4:
240 T).(\lambda (_: (pr3 c t2 t4)).(\lambda (H3: ((\forall (x0: T).((eq T t2
241 (lift h d x0)) \to (\forall (e: C).((drop h d c e) \to (ex2 T (\lambda (t5:
242 T).(eq T t4 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5))))))))).(\lambda
243 (x0: T).(\lambda (H4: (eq T t3 (lift h d x0))).(\lambda (e: C).(\lambda (H5:
244 (drop h d c e)).(let H6 \def (eq_ind T t3 (\lambda (t: T).(pr2 c t t2)) H1
245 (lift h d x0) H4) in (let H7 \def (pr2_gen_lift c x0 t2 h d H6 e H5) in
246 (ex2_ind T (\lambda (t5: T).(eq T t2 (lift h d t5))) (\lambda (t5: T).(pr2 e
247 x0 t5)) (ex2 T (\lambda (t5: T).(eq T t4 (lift h d t5))) (\lambda (t5:
248 T).(pr3 e x0 t5))) (\lambda (x1: T).(\lambda (H8: (eq T t2 (lift h d
249 x1))).(\lambda (H9: (pr2 e x0 x1)).(ex2_ind T (\lambda (t5: T).(eq T t4 (lift
250 h d t5))) (\lambda (t5: T).(pr3 e x1 t5)) (ex2 T (\lambda (t5: T).(eq T t4
251 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5))) (\lambda (x2: T).(\lambda
252 (H10: (eq T t4 (lift h d x2))).(\lambda (H11: (pr3 e x1 x2)).(ex_intro2 T
253 (\lambda (t5: T).(eq T t4 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5)) x2
254 H10 (pr3_sing e x1 x0 H9 x2 H11))))) (H3 x1 H8 e H5))))) H7))))))))))))) y x
258 \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TLRef n) x) \to
259 (or (eq T x (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda
260 (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
261 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
262 (v: T).(eq T x (lift (S n) O v))))))))))
264 \lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr3 c (TLRef
265 n) x)).(insert_eq T (TLRef n) (\lambda (t: T).(pr3 c t x)) (\lambda (t:
266 T).(or (eq T x t) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
267 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
268 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
269 (v: T).(eq T x (lift (S n) O v)))))))) (\lambda (y: T).(\lambda (H0: (pr3 c y
270 x)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).((eq T t (TLRef n)) \to (or
271 (eq T t0 t) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
272 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
273 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
274 (v: T).(eq T t0 (lift (S n) O v)))))))))) (\lambda (t: T).(\lambda (_: (eq T
275 t (TLRef n))).(or_introl (eq T t t) (ex3_3 C T T (\lambda (d: C).(\lambda (u:
276 T).(\lambda (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d:
277 C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda
278 (_: T).(\lambda (v: T).(eq T t (lift (S n) O v)))))) (refl_equal T t))))
279 (\lambda (t2: T).(\lambda (t1: T).(\lambda (H1: (pr2 c t1 t2)).(\lambda (t3:
280 T).(\lambda (H2: (pr3 c t2 t3)).(\lambda (H3: (((eq T t2 (TLRef n)) \to (or
281 (eq T t3 t2) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
282 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
283 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
284 (v: T).(eq T t3 (lift (S n) O v)))))))))).(\lambda (H4: (eq T t1 (TLRef
285 n))).(let H5 \def (eq_ind T t1 (\lambda (t: T).(pr2 c t t2)) H1 (TLRef n) H4)
286 in (eq_ind_r T (TLRef n) (\lambda (t: T).(or (eq T t3 t) (ex3_3 C T T
287 (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead d (Bind
288 Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v))))
289 (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O
290 v)))))))) (let H6 \def (pr2_gen_lref c t2 n H5) in (or_ind (eq T t2 (TLRef
291 n)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl n c (CHead d (Bind Abbr)
292 u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S n) O u))))) (or (eq T
293 t3 (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
294 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
295 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
296 (v: T).(eq T t3 (lift (S n) O v))))))) (\lambda (H7: (eq T t2 (TLRef
297 n))).(let H8 \def (eq_ind T t2 (\lambda (t: T).((eq T t (TLRef n)) \to (or
298 (eq T t3 t) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
299 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
300 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
301 (v: T).(eq T t3 (lift (S n) O v))))))))) H3 (TLRef n) H7) in (let H9 \def
302 (eq_ind T t2 (\lambda (t: T).(pr3 c t t3)) H2 (TLRef n) H7) in (H8
303 (refl_equal T (TLRef n)))))) (\lambda (H7: (ex2_2 C T (\lambda (d:
304 C).(\lambda (u: T).(getl n c (CHead d (Bind Abbr) u)))) (\lambda (_:
305 C).(\lambda (u: T).(eq T t2 (lift (S n) O u)))))).(ex2_2_ind C T (\lambda (d:
306 C).(\lambda (u: T).(getl n c (CHead d (Bind Abbr) u)))) (\lambda (_:
307 C).(\lambda (u: T).(eq T t2 (lift (S n) O u)))) (or (eq T t3 (TLRef n))
308 (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead
309 d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v: T).(pr3 d u
310 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O
311 v))))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H8: (getl n c (CHead x0
312 (Bind Abbr) x1))).(\lambda (H9: (eq T t2 (lift (S n) O x1))).(let H10 \def
313 (eq_ind T t2 (\lambda (t: T).((eq T t (TLRef n)) \to (or (eq T t3 t) (ex3_3 C
314 T T (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead d (Bind
315 Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v))))
316 (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O
317 v))))))))) H3 (lift (S n) O x1) H9) in (let H11 \def (eq_ind T t2 (\lambda
318 (t: T).(pr3 c t t3)) H2 (lift (S n) O x1) H9) in (let H12 \def (pr3_gen_lift
319 c x1 t3 (S n) O H11 x0 (getl_drop Abbr c x0 x1 n H8)) in (ex2_ind T (\lambda
320 (t4: T).(eq T t3 (lift (S n) O t4))) (\lambda (t4: T).(pr3 x0 x1 t4)) (or (eq
321 T t3 (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
322 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
323 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
324 (v: T).(eq T t3 (lift (S n) O v))))))) (\lambda (x2: T).(\lambda (H13: (eq T
325 t3 (lift (S n) O x2))).(\lambda (H14: (pr3 x0 x1 x2)).(or_intror (eq T t3
326 (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl
327 n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v:
328 T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3
329 (lift (S n) O v)))))) (ex3_3_intro C T T (\lambda (d: C).(\lambda (u:
330 T).(\lambda (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d:
331 C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda
332 (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O v))))) x0 x1 x2 H8 H14 H13)))))
333 H12)))))))) H7)) H6)) t1 H4))))))))) y x H0))) H)))).