(plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
(TLRef (plus n h)) (lift n0 O t))) (ty3_abbr g (plus n h) c0 d u
(drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) t H1) (plus
-h (S n)) (plus_comm h (S n))) (lift h d0 (lift (S n) O t)) (lift_free t (S n)
+h (S n)) (plus_sym h (S n))) (lift h d0 (lift (S n) O t)) (lift_free t (S n)
h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
-(plus n (S O)) (plus_comm n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
+(plus n (S O)) (plus_sym n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
d0 H4)))))))))))))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d:
C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda
(t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall
(plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
(TLRef (plus n h)) (lift n0 O u))) (ty3_abst g (plus n h) c0 d u
(drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) t H1) (plus
-h (S n)) (plus_comm h (S n))) (lift h d0 (lift (S n) O u)) (lift_free u (S n)
+h (S n)) (plus_sym h (S n))) (lift h d0 (lift (S n) O u)) (lift_free u (S n)
h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
-(plus n (S O)) (plus_comm n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
+(plus n (S O)) (plus_sym n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (t:
T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
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 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]))
(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 (\lambda (H12: (eq B Abst
-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 Abst
-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 (c0: C).(\lambda (u0: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0
-t0)).(\lambda (H1: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
-nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d: C).(\forall (v:
-T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
-w))))))))))))).(\lambda (b: B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_:
-(ty3 g (CHead c0 (Bind b) u0) t1 t2)).(\lambda (H3: ((\forall (v0:
-T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t1 t3) \to (\forall (b0:
-B).(\forall (d: C).(\forall (v: T).((getl i (CHead c0 (Bind b) u0) (CHead d
-(Bind b0) v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda
-(v0: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead
-(Bind b) u0 t1) t3)).(\lambda (b0: B).(\lambda (d: C).(\lambda (v:
-T).(\lambda (H5: (getl i c0 (CHead d (Bind b0) v))).(or3_ind (ex2 T (\lambda
+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])) (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 (\lambda (H12: (eq B Abst 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 Abst 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 (c0: C).(\lambda
+(u0: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H1:
+((\forall (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 u0 t1) \to
+(\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b)
+v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (b:
+B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b)
+u0) t1 t2)).(\lambda (H3: ((\forall (v0: T).(\forall (t3: T).(\forall (i:
+nat).((subst0 i v0 t1 t3) \to (\forall (b0: B).(\forall (d: C).(\forall (v:
+T).((getl i (CHead c0 (Bind b) u0) (CHead d (Bind b0) v)) \to (ex T (\lambda
+(w: T).(ty3 g d v w))))))))))))).(\lambda (v0: T).(\lambda (t3: T).(\lambda
+(i: nat).(\lambda (H4: (subst0 i v0 (THead (Bind b) u0 t1) t3)).(\lambda (b0:
+B).(\lambda (d: C).(\lambda (v: T).(\lambda (H5: (getl i c0 (CHead d (Bind
+b0) v))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1)))
+(\lambda (u2: T).(subst0 i v0 u0 u2))) (ex2 T (\lambda (t4: T).(eq T t3
+(THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))
+(ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2
+t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_:
+T).(\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))) (ex T (\lambda (w:
+T).(ty3 g d v w))) (\lambda (H6: (ex2 T (\lambda (u2: T).(eq T t3 (THead
+(Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0 u2)))).(ex2_ind T (\lambda
(u2: T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0
-u2))) (ex2 T (\lambda (t4: T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4:
-T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex3_2 T T (\lambda (u2: T).(\lambda
-(t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2: T).(\lambda (_:
-T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Bind b)
-i) v0 t1 t4)))) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (H6: (ex2 T
-(\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i
-v0 u0 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1)))
-(\lambda (u2: T).(subst0 i v0 u0 u2)) (ex T (\lambda (w: T).(ty3 g d v w)))
-(\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b) x t1))).(\lambda (H8:
-(subst0 i v0 u0 x)).(H1 v0 x i H8 b0 d v H5)))) H6)) (\lambda (H6: (ex2 T
+u2)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T
+t3 (THead (Bind b) x t1))).(\lambda (H8: (subst0 i v0 u0 x)).(H1 v0 x i H8 b0
+d v H5)))) H6)) (\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Bind
+b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))).(ex2_ind T
(\lambda (t4: T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0
-(s (Bind b) i) v0 t1 t4)))).(ex2_ind T (\lambda (t4: T).(eq T t3 (THead (Bind
-b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)) (ex T (\lambda
-(w: T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b)
-u0 x))).(\lambda (H8: (subst0 (s (Bind b) i) v0 t1 x)).(H3 v0 x (S i) H8 b0 d
-v (getl_head (Bind b) i c0 (CHead d (Bind b0) v) H5 u0))))) H6)) (\lambda
-(H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2
-t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_:
-T).(\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4))))).(ex3_2_ind T T
-(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda
-(u2: T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4:
+(s (Bind b) i) v0 t1 t4)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x:
+T).(\lambda (_: (eq T t3 (THead (Bind b) u0 x))).(\lambda (H8: (subst0 (s
+(Bind b) i) v0 t1 x)).(H3 v0 x (S i) H8 b0 d v (getl_head (Bind b) i c0
+(CHead d (Bind b0) v) H5 u0))))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2:
+T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2:
+T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4:
+T).(subst0 (s (Bind b) i) v0 t1 t4))))).(ex3_2_ind T T (\lambda (u2:
+T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2:
+T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4:
T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex T (\lambda (w: T).(ty3 g d v w)))
(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t3 (THead (Bind b) x0
x1))).(\lambda (H8: (subst0 i v0 u0 x0)).(\lambda (_: (subst0 (s (Bind b) i)