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 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd".
19 include "pc3/props.ma".
24 \forall (c: C).(\forall (m: nat).(\forall (n: nat).((pc3 c (TSort m) (TSort
25 n)) \to (eq nat m n))))
27 \lambda (c: C).(\lambda (m: nat).(\lambda (n: nat).(\lambda (H: (pc3 c
28 (TSort m) (TSort n))).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr3 c
29 (TSort m) t)) (\lambda (t: T).(pr3 c (TSort n) t)) (eq nat m n) (\lambda (x:
30 T).(\lambda (H1: (pr3 c (TSort m) x)).(\lambda (H2: (pr3 c (TSort n) x)).(let
31 H3 \def (eq_ind T x (\lambda (t: T).(eq T t (TSort n))) (pr3_gen_sort c x n
32 H2) (TSort m) (pr3_gen_sort c x m H1)) in (let H4 \def (f_equal T nat
33 (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort n0)
34 \Rightarrow n0 | (TLRef _) \Rightarrow m | (THead _ _ _) \Rightarrow m]))
35 (TSort m) (TSort n) H3) in H4))))) H0))))).
38 \forall (c: C).(\forall (u1: T).(\forall (u2: T).(\forall (t1: T).(\forall
39 (t2: T).((pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)) \to
40 (land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u)
43 \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (t1: T).(\lambda
44 (t2: T).(\lambda (H: (pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2
45 t2))).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr3 c (THead (Bind Abst)
46 u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2 t2) t)) (land (pc3 c
47 u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u) t1 t2))))
48 (\lambda (x: T).(\lambda (H1: (pr3 c (THead (Bind Abst) u1 t1) x)).(\lambda
49 (H2: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H3 \def (pr3_gen_abst c u2 t2
50 x H2) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
51 (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3)))
52 (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
53 c (Bind b) u) t2 t3))))) (land (pc3 c u1 u2) (\forall (b: B).(\forall (u:
54 T).(pc3 (CHead c (Bind b) u) t1 t2)))) (\lambda (x0: T).(\lambda (x1:
55 T).(\lambda (H4: (eq T x (THead (Bind Abst) x0 x1))).(\lambda (H5: (pr3 c u2
56 x0)).(\lambda (H6: ((\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
57 t2 x1))))).(let H7 \def (pr3_gen_abst c u1 t1 x H1) in (ex3_2_ind T T
58 (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3))))
59 (\lambda (u3: T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda
60 (t3: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t3)))))
61 (land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u)
62 t1 t2)))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T x (THead
63 (Bind Abst) x2 x3))).(\lambda (H9: (pr3 c u1 x2)).(\lambda (H10: ((\forall
64 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 x3))))).(let H11 \def
65 (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind Abst) x0 x1))) H4 (THead
66 (Bind Abst) x2 x3) H8) in (let H12 \def (f_equal T T (\lambda (e: T).(match e
67 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x2 | (TLRef _)
68 \Rightarrow x2 | (THead _ t _) \Rightarrow t])) (THead (Bind Abst) x2 x3)
69 (THead (Bind Abst) x0 x1) H11) in ((let H13 \def (f_equal T T (\lambda (e:
70 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x3 |
71 (TLRef _) \Rightarrow x3 | (THead _ _ t) \Rightarrow t])) (THead (Bind Abst)
72 x2 x3) (THead (Bind Abst) x0 x1) H11) in (\lambda (H14: (eq T x2 x0)).(let
73 H15 \def (eq_ind T x3 (\lambda (t: T).(\forall (b: B).(\forall (u: T).(pr3
74 (CHead c (Bind b) u) t1 t)))) H10 x1 H13) in (let H16 \def (eq_ind T x2
75 (\lambda (t: T).(pr3 c u1 t)) H9 x0 H14) in (conj (pc3 c u1 u2) (\forall (b:
76 B).(\forall (u: T).(pc3 (CHead c (Bind b) u) t1 t2))) (pc3_pr3_t c u1 x0 H16
77 u2 H5) (\lambda (b: B).(\lambda (u: T).(pc3_pr3_t (CHead c (Bind b) u) t1 x1
78 (H15 b u) t2 (H6 b u))))))))) H12)))))))) H7))))))) H3))))) H0))))))).
81 \forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall (h: nat).(\forall
82 (d: nat).((pc3 c (lift h d t1) (lift h d t2)) \to (\forall (e: C).((drop h d
83 c e) \to (pc3 e t1 t2))))))))
85 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (h: nat).(\lambda
86 (d: nat).(\lambda (H: (pc3 c (lift h d t1) (lift h d t2))).(\lambda (e:
87 C).(\lambda (H0: (drop h d c e)).(let H1 \def H in (ex2_ind T (\lambda (t:
88 T).(pr3 c (lift h d t1) t)) (\lambda (t: T).(pr3 c (lift h d t2) t)) (pc3 e
89 t1 t2) (\lambda (x: T).(\lambda (H2: (pr3 c (lift h d t1) x)).(\lambda (H3:
90 (pr3 c (lift h d t2) x)).(let H4 \def (pr3_gen_lift c t2 x h d H3 e H0) in
91 (ex2_ind T (\lambda (t3: T).(eq T x (lift h d t3))) (\lambda (t3: T).(pr3 e
92 t2 t3)) (pc3 e t1 t2) (\lambda (x0: T).(\lambda (H5: (eq T x (lift h d
93 x0))).(\lambda (H6: (pr3 e t2 x0)).(let H7 \def (pr3_gen_lift c t1 x h d H2 e
94 H0) in (ex2_ind T (\lambda (t3: T).(eq T x (lift h d t3))) (\lambda (t3:
95 T).(pr3 e t1 t3)) (pc3 e t1 t2) (\lambda (x1: T).(\lambda (H8: (eq T x (lift
96 h d x1))).(\lambda (H9: (pr3 e t1 x1)).(let H10 \def (eq_ind T x (\lambda (t:
97 T).(eq T t (lift h d x0))) H5 (lift h d x1) H8) in (let H11 \def (eq_ind T x1
98 (\lambda (t: T).(pr3 e t1 t)) H9 x0 (lift_inj x1 x0 h d H10)) in (pc3_pr3_t e
99 t1 x0 H11 t2 H6)))))) H7))))) H4))))) H1))))))))).
101 theorem pc3_gen_not_abst:
102 \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (t1:
103 T).(\forall (t2: T).(\forall (u1: T).(\forall (u2: T).((pc3 c (THead (Bind b)
104 u1 t1) (THead (Bind Abst) u2 t2)) \to (pc3 (CHead c (Bind b) u1) t1 (lift (S
105 O) O (THead (Bind Abst) u2 t2))))))))))
107 \lambda (b: B).(B_ind (\lambda (b0: B).((not (eq B b0 Abst)) \to (\forall
108 (c: C).(\forall (t1: T).(\forall (t2: T).(\forall (u1: T).(\forall (u2:
109 T).((pc3 c (THead (Bind b0) u1 t1) (THead (Bind Abst) u2 t2)) \to (pc3 (CHead
110 c (Bind b0) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))))))))))) (\lambda
111 (_: (not (eq B Abbr Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2:
112 T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Abbr)
113 u1 t1) (THead (Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t:
114 T).(pr3 c (THead (Bind Abbr) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind
115 Abst) u2 t2) t)) (pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind
116 Abst) u2 t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Abbr) u1 t1)
117 x)).(\lambda (H3: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H4 \def
118 (pr3_gen_abbr c u1 t1 x H2) in (or_ind (ex3_2 T T (\lambda (u3: T).(\lambda
119 (t3: T).(eq T x (THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_:
120 T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr3 (CHead c (Bind Abbr)
121 u1) t1 t3)))) (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x)) (pc3 (CHead
122 c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (H5:
123 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abbr) u3
124 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_:
125 T).(\lambda (t3: T).(pr3 (CHead c (Bind Abbr) u1) t1 t3))))).(ex3_2_ind T T
126 (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abbr) u3 t3))))
127 (\lambda (u3: T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda
128 (t3: T).(pr3 (CHead c (Bind Abbr) u1) t1 t3))) (pc3 (CHead c (Bind Abbr) u1)
129 t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0: T).(\lambda (x1:
130 T).(\lambda (H6: (eq T x (THead (Bind Abbr) x0 x1))).(\lambda (_: (pr3 c u1
131 x0)).(\lambda (_: (pr3 (CHead c (Bind Abbr) u1) t1 x1)).(let H9 \def
132 (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3:
133 T).(eq T x (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3
134 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall (u:
135 T).(pr3 (CHead c (Bind b0) u) t2 t3))))) (pc3 (CHead c (Bind Abbr) u1) t1
136 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x2: T).(\lambda (x3:
137 T).(\lambda (H10: (eq T x (THead (Bind Abst) x2 x3))).(\lambda (_: (pr3 c u2
138 x2)).(\lambda (_: ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0)
139 u) t2 x3))))).(let H13 \def (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind
140 Abbr) x0 x1))) H6 (THead (Bind Abst) x2 x3) H10) in (let H14 \def (eq_ind T
141 (THead (Bind Abst) x2 x3) (\lambda (ee: T).(match ee in T return (\lambda (_:
142 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
143 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
144 [(Bind b0) \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr
145 \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
146 _) \Rightarrow False])])) I (THead (Bind Abbr) x0 x1) H13) in (False_ind (pc3
147 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2)))
148 H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3 (CHead c (Bind Abbr) u1) t1
149 (lift (S O) O x))).(let H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T
150 (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3))))
151 (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda
152 (t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2
153 t3))))) (pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2
154 t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind
155 Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0:
156 B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def
157 (eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O
158 t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Abbr) u1)
159 t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind
160 Abst) u2 t2)) (pr3_lift (CHead c (Bind Abbr) u1) c (S O) O (drop_drop (Bind
161 Abbr) O c c (drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0
162 x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6)))
163 H4))))) H1))))))))) (\lambda (H: (not (eq B Abst Abst))).(\lambda (c:
164 C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (u1: T).(\lambda (u2:
165 T).(\lambda (_: (pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2
166 t2))).(let H1 \def (match (H (refl_equal B Abst)) in False return (\lambda
167 (_: False).(pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst)
168 u2 t2)))) with []) in H1)))))))) (\lambda (_: (not (eq B Void
169 Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (u1:
170 T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Void) u1 t1) (THead
171 (Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t: T).(pr3 c
172 (THead (Bind Void) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2
173 t2) t)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2
174 t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Void) u1 t1)
175 x)).(\lambda (H3: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H4 \def
176 (pr3_gen_void c u1 t1 x H2) in (or_ind (ex3_2 T T (\lambda (u3: T).(\lambda
177 (t3: T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_:
178 T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall
179 (u: T).(pr3 (CHead c (Bind b0) u) t1 t3)))))) (pr3 (CHead c (Bind Void) u1)
180 t1 (lift (S O) O x)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead
181 (Bind Abst) u2 t2))) (\lambda (H5: (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
182 T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3
183 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall (u:
184 T).(pr3 (CHead c (Bind b0) u) t1 t3))))))).(ex3_2_ind T T (\lambda (u3:
185 T).(\lambda (t3: T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3:
186 T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall
187 (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t1 t3))))) (pc3 (CHead c
188 (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0:
189 T).(\lambda (x1: T).(\lambda (H6: (eq T x (THead (Bind Void) x0
190 x1))).(\lambda (_: (pr3 c u1 x0)).(\lambda (_: ((\forall (b0: B).(\forall (u:
191 T).(pr3 (CHead c (Bind b0) u) t1 x1))))).(let H9 \def (pr3_gen_abst c u2 t2 x
192 H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind
193 Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_:
194 T).(\lambda (t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0)
195 u) t2 t3))))) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind
196 Abst) u2 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H10: (eq T x
197 (THead (Bind Abst) x2 x3))).(\lambda (_: (pr3 c u2 x2)).(\lambda (_:
198 ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x3))))).(let
199 H13 \def (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind Void) x0 x1))) H6
200 (THead (Bind Abst) x2 x3) H10) in (let H14 \def (eq_ind T (THead (Bind Abst)
201 x2 x3) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
202 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
203 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b0)
204 \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr
205 \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
206 _) \Rightarrow False])])) I (THead (Bind Void) x0 x1) H13) in (False_ind (pc3
207 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2)))
208 H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3 (CHead c (Bind Void) u1) t1
209 (lift (S O) O x))).(let H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T
210 (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3))))
211 (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda
212 (t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2
213 t3))))) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2
214 t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind
215 Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0:
216 B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def
217 (eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O
218 t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Void) u1)
219 t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind
220 Abst) u2 t2)) (pr3_lift (CHead c (Bind Void) u1) c (S O) O (drop_drop (Bind
221 Void) O c c (drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0
222 x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6)))
223 H4))))) H1))))))))) b).
225 theorem pc3_gen_lift_abst:
226 \forall (c: C).(\forall (t: T).(\forall (t2: T).(\forall (u2: T).(\forall
227 (h: nat).(\forall (d: nat).((pc3 c (lift h d t) (THead (Bind Abst) u2 t2))
228 \to (\forall (e: C).((drop h d c e) \to (ex3_2 T T (\lambda (u1: T).(\lambda
229 (t1: T).(pr3 e t (THead (Bind Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_:
230 T).(pr3 c u2 (lift h d u1)))) (\lambda (_: T).(\lambda (t1: T).(\forall (b:
231 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d)
234 \lambda (c: C).(\lambda (t: T).(\lambda (t2: T).(\lambda (u2: T).(\lambda
235 (h: nat).(\lambda (d: nat).(\lambda (H: (pc3 c (lift h d t) (THead (Bind
236 Abst) u2 t2))).(\lambda (e: C).(\lambda (H0: (drop h d c e)).(let H1 \def H
237 in (ex2_ind T (\lambda (t0: T).(pr3 c (lift h d t) t0)) (\lambda (t0: T).(pr3
238 c (THead (Bind Abst) u2 t2) t0)) (ex3_2 T T (\lambda (u1: T).(\lambda (t1:
239 T).(pr3 e t (THead (Bind Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_:
240 T).(pr3 c u2 (lift h d u1)))) (\lambda (_: T).(\lambda (t1: T).(\forall (b:
241 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1)))))))
242 (\lambda (x: T).(\lambda (H2: (pr3 c (lift h d t) x)).(\lambda (H3: (pr3 c
243 (THead (Bind Abst) u2 t2) x)).(let H4 \def (pr3_gen_lift c t x h d H2 e H0)
244 in (ex2_ind T (\lambda (t3: T).(eq T x (lift h d t3))) (\lambda (t3: T).(pr3
245 e t t3)) (ex3_2 T T (\lambda (u1: T).(\lambda (t1: T).(pr3 e t (THead (Bind
246 Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_: T).(pr3 c u2 (lift h d u1))))
247 (\lambda (_: T).(\lambda (t1: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
248 c (Bind b) u) t2 (lift h (S d) t1))))))) (\lambda (x0: T).(\lambda (H5: (eq T
249 x (lift h d x0))).(\lambda (H6: (pr3 e t x0)).(let H7 \def (pr3_gen_abst c u2
250 t2 x H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
251 (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3)))
252 (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
253 c (Bind b) u) t2 t3))))) (ex3_2 T T (\lambda (u1: T).(\lambda (t1: T).(pr3 e
254 t (THead (Bind Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_: T).(pr3 c u2
255 (lift h d u1)))) (\lambda (_: T).(\lambda (t1: T).(\forall (b: B).(\forall
256 (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))))))) (\lambda (x1:
257 T).(\lambda (x2: T).(\lambda (H8: (eq T x (THead (Bind Abst) x1
258 x2))).(\lambda (H9: (pr3 c u2 x1)).(\lambda (H10: ((\forall (b: B).(\forall
259 (u: T).(pr3 (CHead c (Bind b) u) t2 x2))))).(let H11 \def (eq_ind T x
260 (\lambda (t0: T).(eq T t0 (lift h d x0))) H5 (THead (Bind Abst) x1 x2) H8) in
261 (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x0 (THead (Bind Abst) y
262 z)))) (\lambda (y: T).(\lambda (_: T).(eq T x1 (lift h d y)))) (\lambda (_:
263 T).(\lambda (z: T).(eq T x2 (lift h (S d) z)))) (ex3_2 T T (\lambda (u1:
264 T).(\lambda (t1: T).(pr3 e t (THead (Bind Abst) u1 t1)))) (\lambda (u1:
265 T).(\lambda (_: T).(pr3 c u2 (lift h d u1)))) (\lambda (_: T).(\lambda (t1:
266 T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d)
267 t1))))))) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H12: (eq T x0 (THead
268 (Bind Abst) x3 x4))).(\lambda (H13: (eq T x1 (lift h d x3))).(\lambda (H14:
269 (eq T x2 (lift h (S d) x4))).(let H15 \def (eq_ind T x2 (\lambda (t0:
270 T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 t0)))) H10
271 (lift h (S d) x4) H14) in (let H16 \def (eq_ind T x1 (\lambda (t0: T).(pr3 c
272 u2 t0)) H9 (lift h d x3) H13) in (let H17 \def (eq_ind T x0 (\lambda (t0:
273 T).(pr3 e t t0)) H6 (THead (Bind Abst) x3 x4) H12) in (ex3_2_intro T T
274 (\lambda (u1: T).(\lambda (t1: T).(pr3 e t (THead (Bind Abst) u1 t1))))
275 (\lambda (u1: T).(\lambda (_: T).(pr3 c u2 (lift h d u1)))) (\lambda (_:
276 T).(\lambda (t1: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
277 t2 (lift h (S d) t1)))))) x3 x4 H17 H16 H15))))))))) (lift_gen_bind Abst x1
278 x2 x0 h d H11)))))))) H7))))) H4))))) H1)))))))))).