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