-(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(and_ind (eq nat n i)
-(eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w))) (\lambda
-(H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7 \def
-(eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n
-H5) in (let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl
-n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n
-H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C (\lambda (e:
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
-(CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b)
-v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in
-((let H10 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
-C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k
-in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abbr])])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v)
-(getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in
-((let H11 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
-C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2]))
-(CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
-Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (\lambda (H12: (eq B Abbr
-b)).(\lambda (H13: (eq C d d0)).(let H14 \def (eq_ind_r T v (\lambda (t2:
-T).(getl n c0 (CHead d0 (Bind b) t2))) H8 u0 H11) in (eq_ind T u0 (\lambda
-(t2: T).(ex T (\lambda (w: T).(ty3 g d0 t2 w)))) (let H15 \def (eq_ind_r C d0
-(\lambda (c1: C).(getl n c0 (CHead c1 (Bind b) u0))) H14 d H13) in (eq_ind C
-d (\lambda (c1: C).(ex T (\lambda (w: T).(ty3 g c1 u0 w)))) (let H16 \def
-(eq_ind_r B b (\lambda (b0: B).(getl n c0 (CHead d (Bind b0) u0))) H15 Abbr
-H12) in (ex_intro T (\lambda (w: T).(ty3 g d u0 w)) t0 H1)) d0 H13)) v
-H11))))) H10)) H9)))))) (subst0_gen_lref v0 t1 i n H3))))))))))))))))))
-(\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda
-(H0: (getl n c0 (CHead d (Bind Abst) u0))).(\lambda (t0: T).(\lambda (H1:
-(ty3 g d u0 t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
-nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d0: C).(\forall (v:
-T).((getl i d (CHead d0 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v
-w))))))))))))).(\lambda (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
-(H3: (subst0 i v0 (TLRef n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda
-(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(and_ind (eq nat n i)
-(eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w))) (\lambda
-(H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7 \def
-(eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n
-H5) in (let H8 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (c1: C).(getl
-n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n
-H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C (\lambda (e:
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
-(CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abst) u0) (CHead d0 (Bind b)
-v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in
-((let H10 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
-C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k
-in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abst])])) (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v)
-(getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in
-((let H11 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
-C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2]))
+(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(land_ind (eq nat n
+i) (eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w)))
+(\lambda (H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7
+\def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v)))
+H4 n H5) in (let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1:
+C).(getl n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
+Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C
+(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
+\Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0)
+(CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0
+(Bind b) v) H7)) in ((let H10 \def (f_equal C B (\lambda (e: C).(match e in C
+return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
+\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0)
+\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u0)
+(CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0
+(Bind b) v) H7)) in ((let H11 \def (f_equal C T (\lambda (e: C).(match e in C
+return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t2)
+\Rightarrow t2])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v) (getl_mono
+c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (\lambda (H12:
+(eq B Abbr b)).(\lambda (H13: (eq C d d0)).(let H14 \def (eq_ind_r T v
+(\lambda (t2: T).(getl n c0 (CHead d0 (Bind b) t2))) H8 u0 H11) in (eq_ind T
+u0 (\lambda (t2: T).(ex T (\lambda (w: T).(ty3 g d0 t2 w)))) (let H15 \def
+(eq_ind_r C d0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind b) u0))) H14 d
+H13) in (eq_ind C d (\lambda (c1: C).(ex T (\lambda (w: T).(ty3 g c1 u0 w))))
+(let H16 \def (eq_ind_r B b (\lambda (b0: B).(getl n c0 (CHead d (Bind b0)
+u0))) H15 Abbr H12) in (ex_intro T (\lambda (w: T).(ty3 g d u0 w)) t0 H1)) d0
+H13)) v H11))))) H10)) H9)))))) (subst0_gen_lref v0 t1 i n
+H3)))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
+C).(\lambda (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
+u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0 t0)).(\lambda (_: ((\forall
+(v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 u0 t1) \to (\forall
+(b: B).(\forall (d0: C).(\forall (v: T).((getl i d (CHead d0 (Bind b) v)) \to
+(ex T (\lambda (w: T).(ty3 g d0 v w))))))))))))).(\lambda (v0: T).(\lambda
+(t1: T).(\lambda (i: nat).(\lambda (H3: (subst0 i v0 (TLRef n) t1)).(\lambda
+(b: B).(\lambda (d0: C).(\lambda (v: T).(\lambda (H4: (getl i c0 (CHead d0
+(Bind b) v))).(land_ind (eq nat n i) (eq T t1 (lift (S n) O v0)) (ex T
+(\lambda (w: T).(ty3 g d0 v w))) (\lambda (H5: (eq nat n i)).(\lambda (_: (eq
+T t1 (lift (S n) O v0))).(let H7 \def (eq_ind_r nat i (\lambda (n0:
+nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n H5) in (let H8 \def (eq_ind C
+(CHead d (Bind Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead d0 (Bind
+b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7))
+in (let H9 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
+(_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1]))