+ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k
+with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow False | Abst
+\Rightarrow False | Void \Rightarrow True]) | (Flat _) \Rightarrow False])]))
+I (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind Void) x2) n H6
+(CHead x3 (Bind Abst) x4) H10)) in (False_ind False H13))))))))) H8))
+(ty3_gen_lref g c2 t3 n H7)))))) x1 H2))) H4)) (\lambda (H4: ((\forall (t3:
+T).((ty3 g x0 x2 t3) \to False)))).(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 (H5: (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 (H6: (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_ind
+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)))) False (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_:
+(pc3 c2 (lift (S n) O x5) t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abbr)
+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 Abbr) x4)
+(getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in
+(let H11 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) (CHead x0 (Bind x1) x2)
+(CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead
+x3 (Bind Abbr) x4) H8)) in ((let H12 \def (f_equal C B (\lambda (e: C).(match
+e with [(CSort _) \Rightarrow x1 | (CHead _ k _) \Rightarrow (match k with
+[(Bind b) \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 (Bind x1)
+x2) (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2
+(CHead x3 (Bind Abbr) x4) H8)) in ((let H13 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow x2 | (CHead _ _ t) \Rightarrow t]))
+(CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0
+(Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in (\lambda (_: (eq B x1
+Abbr)).(\lambda (H15: (eq C x0 x3)).(let H16 \def (eq_ind_r T x4 (\lambda (t:
+T).(getl n c2 (CHead x3 (Bind Abbr) 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 C x3 (\lambda (c0: C).(getl n c2 (CHead c0 (Bind Abbr) x2))) H16 x0
+H15) in (let H19 \def (eq_ind_r C x3 (\lambda (c0: C).(ty3 g c0 x2 x5)) H17
+x0 H15) in (H4 x5 H19)))))))) H12)) H11))))))))) H6)) (\lambda (H6: (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)))))).(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 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 with [(CSort _) \Rightarrow x1 | (CHead _ k _)
+\Rightarrow (match k 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 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)