-C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))) P (\lambda (x3:
-C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H7: (pc3 c2 (lift (S n) O x4)
-t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abst) x4))).(\lambda (H9: (ty3
-g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind x1) x2) (\lambda (c0:
-C).(getl n c2 c0)) H2 (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind
-x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in (let H11 \def (f_equal C C
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
-\Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) (CHead x0 (Bind x1) x2)
-(CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead
-x3 (Bind Abst) x4) H8)) in ((let H12 \def (f_equal C B (\lambda (e: C).(match
-e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow x1 | (CHead _ k
-_) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 (Bind x1) x2) (CHead
-x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind
-Abst) x4) H8)) in ((let H13 \def (f_equal C T (\lambda (e: C).(match e in C
-return (\lambda (_: C).T) with [(CSort _) \Rightarrow x2 | (CHead _ _ t)
-\Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono
-c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in (\lambda
-(_: (eq B x1 Abst)).(\lambda (H15: (eq C x0 x3)).(let H16 \def (eq_ind_r T x4
-(\lambda (t: T).(getl n c2 (CHead x3 (Bind Abst) t))) H10 x2 H13) in (let H17
-\def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) H9 x2 H13) in (let H18
-\def (eq_ind_r T x4 (\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)) H7 x2 H13)
-in (let H19 \def (eq_ind_r C x3 (\lambda (c0: C).(getl n c2 (CHead c0 (Bind
-Abst) x2))) H16 x0 H15) in (let H20 \def (eq_ind_r C x3 (\lambda (c0: C).(ty3
-g c0 x2 x5)) H17 x0 H15) in (H4 x5 H20 P))))))))) H12)) H11))))))))) H6))
-(ty3_gen_lref g c2 t3 n H5))))))) H3)))))) H1)) (\lambda (H1: ((\forall (d:
-C).((getl n c2 d) \to (\forall (P: Prop).P))))).(or_intror (ex T (\lambda
-(t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef n) t3)
-\to (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H2: (ty3 g c2 (TLRef
-n) t3)).(\lambda (P: Prop).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))))).(ex3_3_ind C T T
+(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u)
+t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
+(Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
+t)))) False (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H7:
+(pc3 c2 (lift (S n) O x4) t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abst)
+x4))).(\lambda (H9: (ty3 g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind
+x1) x2) (\lambda (c0: C).(getl n c2 c0)) H2 (CHead x3 (Bind Abst) x4)
+(getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in
+(let H11 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_:
+C).C) with [(CSort _) \Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0]))
+(CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0
+(Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in ((let H12 \def (f_equal
+C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
+\Rightarrow x1 | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_:
+K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0
+(Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2)
+n H2 (CHead x3 (Bind Abst) x4) H8)) in ((let H13 \def (f_equal C T (\lambda
+(e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow x2
+| (CHead _ _ t) \Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind
+Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst)
+x4) H8)) in (\lambda (_: (eq B x1 Abst)).(\lambda (H15: (eq C x0 x3)).(let
+H16 \def (eq_ind_r T x4 (\lambda (t: T).(getl n c2 (CHead x3 (Bind Abst) t)))
+H10 x2 H13) in (let H17 \def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5))
+H9 x2 H13) in (let H18 \def (eq_ind_r T x4 (\lambda (t: T).(pc3 c2 (lift (S
+n) O t) t3)) H7 x2 H13) in (let H19 \def (eq_ind_r C x3 (\lambda (c0:
+C).(getl n c2 (CHead c0 (Bind Abst) x2))) H16 x0 H15) in (let H20 \def
+(eq_ind_r C x3 (\lambda (c0: C).(ty3 g c0 x2 x5)) H17 x0 H15) in (H4 x5
+H20))))))))) H12)) H11))))))))) H6)) (ty3_gen_lref g c2 t3 n H5))))))
+H3)))))) H1)) (\lambda (H1: ((\forall (d: C).((getl n c2 d) \to (\forall (P:
+Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
+(\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to False)) (\lambda (t3:
+T).(\lambda (H2: (ty3 g c2 (TLRef n) t3)).(or_ind (ex3_3 C T T (\lambda (_:
+C).(\lambda (_: T).(\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda
+(e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u)))))
+(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T
+T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u)
+t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
+(Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
+t))))) False (\lambda (H3: (ex3_3 C T T (\lambda (_: C).(\lambda (_: