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/ex1/props".
19 include "ex1/defs.ma".
27 include "nf2/props.ma".
29 include "arity/defs.ma".
31 include "leq/props.ma".
33 theorem ex1__leq_sort_SS:
34 \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc
35 g (asucc g (ASort (S (S k)) n))))))
37 \lambda (g: G).(\lambda (k: nat).(\lambda (n: nat).(leq_refl g (asucc g
38 (asucc g (ASort (S (S k)) n)))))).
41 \forall (g: G).(arity g ex1_c ex1_t (ASort O O))
43 \lambda (g: G).(arity_appl g (CHead (CHead (CHead (CSort O) (Bind Abst)
44 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef O) (ASort (S
45 (S O)) O) (arity_abst g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
46 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind
47 Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O) O (getl_refl Abst (CHead
48 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O))
49 (ASort (S (S O)) O) (arity_abst g (CHead (CHead (CSort O) (Bind Abst) (TSort
50 O)) (Bind Abst) (TSort O)) (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O)
51 O (getl_refl Abst (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O)) (asucc g
52 (ASort (S (S O)) O)) (arity_repl g (CHead (CSort O) (Bind Abst) (TSort O))
53 (TSort O) (ASort O O) (arity_sort g (CHead (CSort O) (Bind Abst) (TSort O))
54 O) (asucc g (asucc g (ASort (S (S O)) O))) (ex1__leq_sort_SS g O O)))) (THead
55 (Bind Abst) (TLRef (S (S O))) (TSort O)) (ASort O O) (arity_head g (CHead
56 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
57 Abst) (TLRef O)) (TLRef (S (S O))) (ASort (S (S O)) O) (arity_abst g (CHead
58 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
59 Abst) (TLRef O)) (CSort O) (TSort O) (S (S O)) (getl_clear_bind Abst (CHead
60 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
61 Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
62 (TSort O)) (TLRef O) (clear_bind Abst (CHead (CHead (CSort O) (Bind Abst)
63 (TSort O)) (Bind Abst) (TSort O)) (TLRef O)) (CHead (CSort O) (Bind Abst)
64 (TSort O)) (S O) (getl_head (Bind Abst) O (CHead (CSort O) (Bind Abst) (TSort
65 O)) (CHead (CSort O) (Bind Abst) (TSort O)) (getl_refl Abst (CSort O) (TSort
66 O)) (TSort O))) (asucc g (ASort (S (S O)) O)) (arity_repl g (CSort O) (TSort
67 O) (ASort O O) (arity_sort g (CSort O) O) (asucc g (asucc g (ASort (S (S O))
68 O))) (ex1__leq_sort_SS g O O))) (TSort O) (ASort O O) (arity_sort g (CHead
69 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
70 (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) O))).
73 \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P:
76 \lambda (g: G).(\lambda (u: T).(\lambda (H: (ty3 g (CHead (CHead (CHead
77 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
78 O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort
79 O))) u)).(\lambda (P: Prop).(ex3_2_ind T T (\lambda (u0: T).(\lambda (t:
80 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
81 (TSort O)) (Bind Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind
82 Abst) u0 t)) u))) (\lambda (u0: T).(\lambda (t: T).(ty3 g (CHead (CHead
83 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
84 (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) (THead (Bind Abst)
85 u0 t)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CSort
86 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
87 (TLRef O) u0))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 (CHead
88 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
89 Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) x0 x1))
90 u)).(\lambda (H1: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
91 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef
92 (S (S O))) (TSort O)) (THead (Bind Abst) x0 x1))).(\lambda (H2: (ty3 g (CHead
93 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
94 Abst) (TLRef O)) (TLRef O) x0)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda
95 (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
96 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O t) x0))))
97 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead
98 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
99 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
100 (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
101 T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
102 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0))))
103 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead
104 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
105 O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
106 (t: T).(ty3 g e u0 t))))) P (\lambda (H3: (ex3_3 C T T (\lambda (_:
107 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
108 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O
109 t) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead
110 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
111 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
112 T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_:
113 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
114 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O
115 t) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead
116 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
117 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
118 T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2: C).(\lambda (x3:
119 T).(\lambda (x4: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind
120 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O
121 x4) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort O) (Bind Abst)
122 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind
123 Abbr) x3))).(\lambda (_: (ty3 g x2 x3 x4)).(ex4_3_ind T T T (\lambda (t2:
124 T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
125 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind
126 Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1))))) (\lambda (_:
127 T).(\lambda (t: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CSort O)
128 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
129 (S (S O))) t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
130 (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
131 (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O)
132 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead (CHead
133 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
134 Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) t2 t0)))) P (\lambda (x5:
135 T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (_: (pc3 (CHead (CHead (CHead
136 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
137 O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0
138 x1))).(\lambda (H8: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
139 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
140 x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst)
141 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef
142 (S (S O)))) (TSort O) x5)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead
143 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
144 O)) (Bind Abst) (TLRef (S (S O)))) x5 x7)).(or_ind (ex3_3 C T T (\lambda (_:
145 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
146 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
147 O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S
148 O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
149 O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e:
150 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda
151 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O)
152 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S
153 (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
154 T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
155 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0)))))
156 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P
157 (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
158 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
159 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda
160 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead
161 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
162 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
163 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
164 T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
165 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6))))
166 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead
167 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
168 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
169 T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9:
170 T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind
171 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
172 O))) O x10) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort
173 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
174 (CHead x8 (Bind Abbr) x9))).(\lambda (_: (ty3 g x8 x9 x10)).(let H15 \def
175 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
176 (TSort O)) (CHead x8 (Bind Abbr) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind
177 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
178 (CHead x8 (Bind Abbr) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e:
179 C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
180 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abbr) x9))) P
181 (\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind
182 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x8
183 (Bind Abbr) x9))).(let H18 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda
184 (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
185 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
186 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
187 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
188 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead
189 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
190 O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
191 Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead
192 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
193 Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H18)))))
194 H15)))))))) H11)) (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
195 T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
196 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0)
197 x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O))
198 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
199 (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda
200 (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_:
201 C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
202 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
203 O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S
204 (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
205 (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e:
206 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8:
207 C).(\lambda (x9: T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead
208 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
209 O)) (lift (S (S (S O))) O x9) x6)).(\lambda (H13: (getl (S (S O)) (CHead
210 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
211 Abst) (TLRef O)) (CHead x8 (Bind Abst) x9))).(\lambda (_: (ty3 g x8 x9
212 x10)).(let H15 \def (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort
213 O)) (Bind Abst) (TSort O)) (CHead x8 (Bind Abst) x9) (r (Bind Abst) (S O))
214 (getl_gen_S (Bind Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
215 Abst) (TSort O)) (CHead x8 (Bind Abst) x9) (TLRef O) (S O) H13)) in (ex2_ind
216 C (\lambda (e: C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort
217 O)) (Bind Abst) (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abst)
218 x9))) P (\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O)
219 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x
220 (CHead x8 (Bind Abst) x9))).(let H18 \def (eq_ind C (CHead x2 (Bind Abbr) x3)
221 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
222 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
223 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
224 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
225 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead
226 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
227 O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
228 Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead
229 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
230 Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H18)))))
231 H15)))))))) H11)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst)
232 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x6 (S (S O))
233 H8))))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort O) (Bind Abst)
234 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
235 (TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3)) (\lambda (H3: (ex3_3 C T
236 T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead
237 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
238 O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
239 T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
240 (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e:
241 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T
242 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead
243 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
244 O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
245 T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
246 (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e:
247 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2:
248 C).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H4: (pc3 (CHead (CHead (CHead
249 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
250 O)) (lift (S O) O x3) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort
251 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
252 (CHead x2 (Bind Abst) x3))).(\lambda (H6: (ty3 g x2 x3 x4)).(ex4_3_ind T T T
253 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead
254 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
255 O)) (THead (Bind Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1)))))
256 (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead
257 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
258 O)) (TLRef (S (S O))) t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_:
259 T).(ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
260 Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort
261 O) t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead
262 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
263 (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) t2 t0)))) P (\lambda
264 (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (H7: (pc3 (CHead (CHead
265 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
266 (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0
267 x1))).(\lambda (H8: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
268 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
269 x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst)
270 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef
271 (S (S O)))) (TSort O) x5)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead
272 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
273 O)) (Bind Abst) (TLRef (S (S O)))) x5 x7)).(or_ind (ex3_3 C T T (\lambda (_:
274 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
275 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
276 O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S
277 O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
278 O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e:
279 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda
280 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O)
281 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S
282 (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
283 T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
284 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0)))))
285 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P
286 (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
287 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
288 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda
289 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead
290 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
291 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
292 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
293 T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
294 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6))))
295 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead
296 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
297 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
298 T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9:
299 T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind
300 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
301 O))) O x10) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort
302 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
303 (CHead x8 (Bind Abbr) x9))).(\lambda (_: (ty3 g x8 x9 x10)).(let H15 \def
304 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
305 (TSort O)) (CHead x8 (Bind Abbr) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind
306 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
307 (CHead x8 (Bind Abbr) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e:
308 C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
309 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abbr) x9))) P
310 (\lambda (x: C).(\lambda (H16: (drop (S O) O (CHead (CHead (CSort O) (Bind
311 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H17: (clear x (CHead x8
312 (Bind Abbr) x9))).(let H18 \def (f_equal C C (\lambda (e: C).(match e in C
313 return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _)
314 \Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O)
315 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
316 (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
317 Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead
318 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
319 Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H19 \def (f_equal C
320 T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
321 \Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3)
322 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
323 (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind
324 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O)
325 (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
326 (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in (\lambda
327 (H20: (eq C x2 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
328 (TSort O)))).(let H21 \def (eq_ind T x3 (\lambda (t: T).(ty3 g x2 t x4)) H6
329 (TLRef O) H19) in (let H22 \def (eq_ind T x3 (\lambda (t: T).(pc3 (CHead
330 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
331 Abst) (TLRef O)) (lift (S O) O t) x0)) H4 (TLRef O) H19) in (let H23 \def
332 (eq_ind C x2 (\lambda (c: C).(ty3 g c (TLRef O) x4)) H21 (CHead (CHead (CSort
333 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H20) in (let H24 \def
334 (eq_ind_r C x (\lambda (c: C).(clear c (CHead x8 (Bind Abbr) x9))) H17 (CHead
335 (CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst)
336 (TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort
337 O)) x (TSort O) O H16))) in (let H25 \def (eq_ind C (CHead x8 (Bind Abbr) x9)
338 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
339 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
340 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
341 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
342 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CSort O)
343 (Bind Abst) (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abbr)
344 x9) (TSort O) H24)) in (False_ind P H25)))))))) H18))))) H15)))))))) H11))
345 (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
346 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
347 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda
348 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead
349 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
350 O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
351 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0:
352 T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
353 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0)
354 x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O))
355 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
356 (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda
357 (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9:
358 T).(\lambda (x10: T).(\lambda (H12: (pc3 (CHead (CHead (CHead (CSort O) (Bind
359 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
360 O))) O x9) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort O)
361 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead
362 x8 (Bind Abst) x9))).(\lambda (H14: (ty3 g x8 x9 x10)).(let H15 \def
363 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
364 (TSort O)) (CHead x8 (Bind Abst) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind
365 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
366 (CHead x8 (Bind Abst) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e:
367 C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
368 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abst) x9))) P
369 (\lambda (x: C).(\lambda (H16: (drop (S O) O (CHead (CHead (CSort O) (Bind
370 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H17: (clear x (CHead x8
371 (Bind Abst) x9))).(let H18 \def (f_equal C C (\lambda (e: C).(match e in C
372 return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _)
373 \Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O)
374 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
375 (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
376 Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead
377 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
378 Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H19 \def (f_equal C
379 T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
380 \Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3)
381 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
382 (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind
383 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O)
384 (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
385 (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in (\lambda
386 (H20: (eq C x2 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
387 (TSort O)))).(let H21 \def (eq_ind T x3 (\lambda (t: T).(ty3 g x2 t x4)) H6
388 (TLRef O) H19) in (let H22 \def (eq_ind T x3 (\lambda (t: T).(pc3 (CHead
389 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
390 Abst) (TLRef O)) (lift (S O) O t) x0)) H4 (TLRef O) H19) in (let H23 \def
391 (eq_ind C x2 (\lambda (c: C).(ty3 g c (TLRef O) x4)) H21 (CHead (CHead (CSort
392 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H20) in (let H24 \def
393 (eq_ind_r C x (\lambda (c: C).(clear c (CHead x8 (Bind Abst) x9))) H17 (CHead
394 (CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst)
395 (TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort
396 O)) x (TSort O) O H16))) in (let H25 \def (f_equal C C (\lambda (e: C).(match
397 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow x8 | (CHead c _
398 _) \Rightarrow c])) (CHead x8 (Bind Abst) x9) (CHead (CSort O) (Bind Abst)
399 (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abst) x9) (TSort O)
400 H24)) in ((let H26 \def (f_equal C T (\lambda (e: C).(match e in C return
401 (\lambda (_: C).T) with [(CSort _) \Rightarrow x9 | (CHead _ _ t) \Rightarrow
402 t])) (CHead x8 (Bind Abst) x9) (CHead (CSort O) (Bind Abst) (TSort O))
403 (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abst) x9) (TSort O) H24)) in
404 (\lambda (H27: (eq C x8 (CSort O))).(let H28 \def (eq_ind T x9 (\lambda (t:
405 T).(ty3 g x8 t x10)) H14 (TSort O) H26) in (let H29 \def (eq_ind T x9
406 (\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
407 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6))
408 H12 (TSort O) H26) in (let H30 \def (eq_ind C x8 (\lambda (c: C).(ty3 g c
409 (TSort O) x10)) H28 (CSort O) H27) in (or_ind (ex3_3 C T T (\lambda (_:
410 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst)
411 (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e:
412 C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind
413 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda
414 (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T
415 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O)
416 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4))))
417 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort
418 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0)))))
419 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P
420 (\lambda (H31: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
421 T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
422 (lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
423 T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
424 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
425 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
426 T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
427 Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0:
428 T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O))
429 (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda
430 (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x11: C).(\lambda (x12:
431 T).(\lambda (x13: T).(\lambda (_: (pc3 (CHead (CHead (CSort O) (Bind Abst)
432 (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x13) x4)).(\lambda (H33:
433 (getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
434 (CHead x11 (Bind Abbr) x12))).(\lambda (_: (ty3 g x11 x12 x13)).(let H35 \def
435 (eq_ind C (CHead x11 (Bind Abbr) x12) (\lambda (ee: C).(match ee in C return
436 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
437 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
438 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
439 True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _)
440 \Rightarrow False])])) I (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
441 Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O) (Bind Abst) (TSort O))
442 (CHead x11 (Bind Abbr) x12) (TSort O) (getl_gen_O (CHead (CHead (CSort O)
443 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x11 (Bind Abbr) x12)
444 H33))) in (False_ind P H35)))))))) H31)) (\lambda (H31: (ex3_3 C T T (\lambda
445 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O) (Bind
446 Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4)))) (\lambda (e:
447 C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind
448 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0))))) (\lambda
449 (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T
450 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O)
451 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4))))
452 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort
453 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0)))))
454 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda
455 (x11: C).(\lambda (x12: T).(\lambda (x13: T).(\lambda (H32: (pc3 (CHead
456 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O
457 x12) x4)).(\lambda (H33: (getl O (CHead (CHead (CSort O) (Bind Abst) (TSort
458 O)) (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12))).(\lambda (H34: (ty3
459 g x11 x12 x13)).(let H35 \def (f_equal C C (\lambda (e: C).(match e in C
460 return (\lambda (_: C).C) with [(CSort _) \Rightarrow x11 | (CHead c _ _)
461 \Rightarrow c])) (CHead x11 (Bind Abst) x12) (CHead (CHead (CSort O) (Bind
462 Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O)
463 (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12) (TSort O) (getl_gen_O
464 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead
465 x11 (Bind Abst) x12) H33))) in ((let H36 \def (f_equal C T (\lambda (e:
466 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow x12 |
467 (CHead _ _ t) \Rightarrow t])) (CHead x11 (Bind Abst) x12) (CHead (CHead
468 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst
469 (CHead (CSort O) (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12) (TSort O)
470 (getl_gen_O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
471 O)) (CHead x11 (Bind Abst) x12) H33))) in (\lambda (H37: (eq C x11 (CHead
472 (CSort O) (Bind Abst) (TSort O)))).(let H38 \def (eq_ind T x12 (\lambda (t:
473 T).(ty3 g x11 t x13)) H34 (TSort O) H36) in (let H39 \def (eq_ind T x12
474 (\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
475 Abst) (TSort O)) (lift (S O) O t) x4)) H32 (TSort O) H36) in (let H40 \def
476 (eq_ind C x11 (\lambda (c: C).(ty3 g c (TSort O) x13)) H38 (CHead (CSort O)
477 (Bind Abst) (TSort O)) H37) in (and_ind (pc3 (CHead (CHead (CHead (CSort O)
478 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
479 (S (S O))) x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead
480 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
481 (TLRef O)) (Bind b) u0) x5 x1))) P (\lambda (H41: (pc3 (CHead (CHead (CHead
482 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
483 O)) (TLRef (S (S O))) x0)).(\lambda (_: ((\forall (b: B).(\forall (u0:
484 T).(pc3 (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
485 Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind b) u0) x5 x1))))).(let H43 \def
486 (eq_ind T (lift (S O) O (TLRef O)) (\lambda (t: T).(pc3 (CHead (CHead (CHead
487 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
488 O)) (TLRef (S (S O))) t)) (pc3_t x0 (CHead (CHead (CHead (CSort O) (Bind
489 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S
490 O))) H41 (lift (S O) O (TLRef O)) (ex2_sym T (pr3 (CHead (CHead (CHead (CSort
491 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift
492 (S O) O (TLRef O))) (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
493 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x0) H22)) (TLRef (plus O (S
494 O))) (lift_lref_ge O (S O) O (le_n O))) in (let H44 \def H43 in (ex2_ind T
495 (\lambda (t: T).(pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
496 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) t)) (\lambda
497 (t: T).(pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
498 (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) t)) P (\lambda (x14:
499 T).(\lambda (H45: (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
500 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
501 x14)).(\lambda (H46: (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
502 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) x14)).(let
503 H47 \def (eq_ind_r T x14 (\lambda (t: T).(eq T (TLRef (S (S O))) t))
504 (nf2_pr3_unfold (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
505 Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x14 H45
506 (nf2_lref_abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
507 Abst) (TSort O)) (Bind Abst) (TLRef O)) (CSort O) (TSort O) (S (S O))
508 (getl_clear_bind Abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
509 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind
510 Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O) (clear_bind Abst (CHead
511 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O))
512 (CHead (CSort O) (Bind Abst) (TSort O)) (S O) (getl_head (Bind Abst) O (CHead
513 (CSort O) (Bind Abst) (TSort O)) (CHead (CSort O) (Bind Abst) (TSort O))
514 (getl_refl Abst (CSort O) (TSort O)) (TSort O))))) (TLRef (S O))
515 (nf2_pr3_unfold (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
516 Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) x14 H46 (nf2_lref_abst
517 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
518 (Bind Abst) (TLRef O)) (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O) (S
519 O) (getl_head (Bind Abst) O (CHead (CHead (CSort O) (Bind Abst) (TSort O))
520 (Bind Abst) (TSort O)) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
521 Abst) (TSort O)) (getl_refl Abst (CHead (CSort O) (Bind Abst) (TSort O))
522 (TSort O)) (TLRef O))))) in (let H48 \def (eq_ind T (TLRef (S (S O)))
523 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
524 \Rightarrow False | (TLRef n) \Rightarrow (match n in nat return (\lambda (_:
525 nat).Prop) with [O \Rightarrow False | (S n0) \Rightarrow (match n0 in nat
526 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
527 True])]) | (THead _ _ _) \Rightarrow False])) I (TLRef (S O)) H47) in
528 (False_ind P H48)))))) H44))))) (pc3_gen_abst (CHead (CHead (CHead (CSort O)
529 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
530 (S (S O))) x0 x5 x1 H7))))))) H35)))))))) H31)) (ty3_gen_lref g (CHead (CHead
531 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x4 O H23)))))))
532 H25)))))))) H18))))) H15)))))))) H11)) (ty3_gen_lref g (CHead (CHead (CHead
533 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
534 O)) x6 (S (S O)) H8))))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort
535 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
536 (TLRef (S (S O))) (TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3))
537 (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
538 Abst) (TSort O)) (Bind Abst) (TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead
539 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
540 Abst) (TLRef O)) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u