+x7 (Bind Abst) x8) (r (Bind Abst) (S O)) (getl_gen_S (Bind Abst) (CHead
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x7
+(Bind Abst) x8) (TLRef O) (S O) H12)) in (ex2_ind C (\lambda (e: C).(drop (S
+O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
+e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abst) x8))) P (\lambda (x:
+C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O))
+(Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x7 (Bind Abst)
+x8))).(let H17 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda (ee:
+C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow
+(match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True |
+Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow
+False])])) I (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abbr)
+x3) (TLRef O) (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3)
+H5))) in (False_ind P H17))))) H14)))))))) H10)) (ty3_gen_lref g (CHead
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
+Abst) (TLRef O)) x6 (S (S O)) H8))))))) (ty3_gen_bind g Abst (CHead (CHead
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
+(TLRef O)) (TLRef (S (S O))) (TSort O) (THead (Bind Abst) x0 x1) H1))))))))
+H3)) (\lambda (H3: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0)))) (\lambda (e:
+C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead (CSort O)
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e
+(Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e
+u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0)))) (\lambda (e:
+C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead (CSort O)
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e
+(Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e
+u0 t)))) P (\lambda (x2: C).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H4:
+(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
+O)) (Bind Abst) (TLRef O)) (lift (S O) O x3) x0)).(\lambda (H5: (getl O
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
+(Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3))).(\lambda (H6: (ty3 g x2 x3
+x4)).(ex3_2_ind T T (\lambda (t2: T).(\lambda (_: T).(pc3 (CHead (CHead
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
+(TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0
+x1)))) (\lambda (_: T).(\lambda (t: T).(ty3 g (CHead (CHead (CHead (CSort O)
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
+(S (S O))) t))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
+(TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) t2))) P (\lambda (x5:
+T).(\lambda (x6: T).(\lambda (H7: (pc3 (CHead (CHead (CHead (CSort O) (Bind
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind
+Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0 x1))).(\lambda (H8: (ty3 g
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
+(Bind Abst) (TLRef O)) (TLRef (S (S O))) x6)).(\lambda (_: (ty3 g (CHead
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
+(Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) x5)).(or_ind
+(ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
+Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda (e: C).(\lambda
+(u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind
+Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0
+t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3