-(y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) (eq_ind_r nat (plus (minus n (S
-O)) (S O)) (\lambda (n0: nat).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq
-T (TLRef n0) (lift (S O) d0 y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T
-(lift (S n) O t) (lift (S O) d0 y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
-g a y1 y2))))) (ex3_2_intro T T (\lambda (y1: T).(\lambda (_: T).(eq T (TLRef
-(plus (minus n (S O)) (S O))) (lift (S O) d0 y1)))) (\lambda (_: T).(\lambda
-(y2: T).(eq T (lift (S n) O t) (lift (S O) d0 y2)))) (\lambda (y1:
-T).(\lambda (y2: T).(ty3 g a y1 y2))) (TLRef (minus n (S O))) (lift n O t)
-(eq_ind_r T (TLRef (plus (minus n (S O)) (S O))) (\lambda (t0: T).(eq T
-(TLRef (plus (minus n (S O)) (S O))) t0)) (refl_equal T (TLRef (plus (minus n
-(S O)) (S O)))) (lift (S O) d0 (TLRef (minus n (S O)))) (lift_lref_ge (minus
-n (S O)) (S O) d0 (lt_le_minus d0 n H5))) (eq_ind_r T (lift (plus (S O) n) O
-t) (\lambda (t0: T).(eq T (lift (S n) O t) t0)) (refl_equal T (lift (S n) O
-t)) (lift (S O) d0 (lift n O t)) (lift_free t n (S O) O d0 (le_S_n d0 (plus O
-n) (le_S (S d0) (plus O n) H5)) (le_O_n d0))) (eq_ind_r nat (S (minus n (S
-O))) (\lambda (n0: nat).(ty3 g a (TLRef (minus n (S O))) (lift n0 O t)))
-(ty3_abbr g (minus n (S O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abbr)
-u) c0 H0 a (S O) d0 H4 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le
-n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n
-(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O))) (plus_sym
-(S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus
-O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
-H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
-C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
-u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (e:
-C).(\forall (u0: T).(\forall (d0: nat).((getl d0 d (CHead e (Bind Void) u0))
-\to (\forall (a: C).((drop (S O) d0 d a) \to (ex3_2 T T (\lambda (y1:
-T).(\lambda (_: T).(eq T u (lift (S O) d0 y1)))) (\lambda (_: T).(\lambda
-(y2: T).(eq T t (lift (S O) d0 y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
-g a y1 y2)))))))))))).(\lambda (e: C).(\lambda (u0: T).(\lambda (d0:
-nat).(\lambda (H3: (getl d0 c0 (CHead e (Bind Void) u0))).(\lambda (a:
-C).(\lambda (H4: (drop (S O) d0 c0 a)).(lt_eq_gt_e n d0 (ex3_2 T T (\lambda
-(y1: T).(\lambda (_: T).(eq T (TLRef n) (lift (S O) d0 y1)))) (\lambda (_:
-T).(\lambda (y2: T).(eq T (lift (S n) O u) (lift (S O) d0 y2)))) (\lambda
-(y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (H5: (lt n d0)).(let H6
-\def (eq_ind nat (minus d0 n) (\lambda (n0: nat).(getl n0 (CHead d (Bind
-Abst) u) (CHead e (Bind Void) u0))) (getl_conf_le d0 (CHead e (Bind Void) u0)
-c0 H3 (CHead d (Bind Abst) u) n H0 (le_S_n n d0 (le_S (S n) d0 H5))) (S
-(minus d0 (S n))) (minus_x_Sy d0 n H5)) in (let H7 \def (eq_ind nat d0
-(\lambda (n0: nat).(drop (S O) n0 c0 a)) H4 (S (plus n (minus d0 (S n))))
-(lt_plus_minus n d0 H5)) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
-C).(eq T u (lift (S O) (minus d0 (S n)) v)))) (\lambda (v: T).(\lambda (e0:
-C).(getl n a (CHead e0 (Bind Abst) v)))) (\lambda (_: T).(\lambda (e0:
-C).(drop (S O) (minus d0 (S n)) d e0))) (ex3_2 T T (\lambda (y1: T).(\lambda
+(y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) (ex3_2_intro T T (\lambda (y1:
+T).(\lambda (_: T).(eq T (TLRef (plus (minus n (S O)) (S O))) (lift (S O) d0
+y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S n) O t) (lift (S O) d0
+y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (TLRef (minus n (S
+O))) (lift n O t) (eq_ind_r T (TLRef (plus (minus n (S O)) (S O))) (\lambda
+(t0: T).(eq T (TLRef (plus (minus n (S O)) (S O))) t0)) (refl_equal T (TLRef
+(plus (minus n (S O)) (S O)))) (lift (S O) d0 (TLRef (minus n (S O))))
+(lift_lref_ge (minus n (S O)) (S O) d0 (lt_le_minus d0 n H5))) (eq_ind_r T
+(lift (plus (S O) n) O t) (\lambda (t0: T).(eq T (lift (S n) O t) t0))
+(refl_equal T (lift (S n) O t)) (lift (S O) d0 (lift n O t)) (lift_free t n
+(S O) O d0 (le_S_n d0 (plus O n) (le_S (S d0) (plus O n) H5)) (le_O_n d0)))
+(eq_ind_r nat (S (minus n (S O))) (\lambda (n0: nat).(ty3 g a (TLRef (minus n
+(S O))) (lift n0 O t))) (ty3_abbr g (minus n (S O)) a d u (getl_drop_conf_ge
+n (CHead d (Bind Abbr) u) c0 H0 a (S O) d0 H4 (eq_ind_r nat (plus (S O) d0)
+(\lambda (n0: nat).(le n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1)
+n (minus_x_SO n (le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n
+(S O))) (plus_sym (S O) (minus n (S O)))) (S (plus O (minus n (S O))))
+(refl_equal nat (S (plus O (minus n (S O)))))) n (lt_plus_minus O n
+(le_lt_trans O d0 n (le_O_n d0) H5))))))))))))))))))) (\lambda (n:
+nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n
+c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
+t)).(\lambda (H2: ((\forall (e: C).(\forall (u0: T).(\forall (d0: nat).((getl
+d0 d (CHead e (Bind Void) u0)) \to (\forall (a: C).((drop (S O) d0 d a) \to
+(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T u (lift (S O) d0 y1))))
+(\lambda (_: T).(\lambda (y2: T).(eq T t (lift (S O) d0 y2)))) (\lambda (y1:
+T).(\lambda (y2: T).(ty3 g a y1 y2)))))))))))).(\lambda (e: C).(\lambda (u0:
+T).(\lambda (d0: nat).(\lambda (H3: (getl d0 c0 (CHead e (Bind Void)
+u0))).(\lambda (a: C).(\lambda (H4: (drop (S O) d0 c0 a)).(lt_eq_gt_e n d0
+(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (TLRef n) (lift (S O) d0
+y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S n) O u) (lift (S O) d0
+y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (H5: (lt
+n d0)).(let H6 \def (eq_ind nat (minus d0 n) (\lambda (n0: nat).(getl n0
+(CHead d (Bind Abst) u) (CHead e (Bind Void) u0))) (getl_conf_le d0 (CHead e
+(Bind Void) u0) c0 H3 (CHead d (Bind Abst) u) n H0 (le_S_n n d0 (le_S_n (S n)
+(S d0) (le_S (S (S n)) (S d0) (le_n_S (S n) d0 H5))))) (S (minus d0 (S n)))
+(minus_x_Sy d0 n H5)) in (let H7 \def (eq_ind nat d0 (\lambda (n0: nat).(drop
+(S O) n0 c0 a)) H4 (S (plus n (minus d0 (S n)))) (lt_plus_minus n d0 H5)) in
+(ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift (S O) (minus d0
+(S n)) v)))) (\lambda (v: T).(\lambda (e0: C).(getl n a (CHead e0 (Bind Abst)
+v)))) (\lambda (_: T).(\lambda (e0: C).(drop (S O) (minus d0 (S n)) d e0)))
+(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (TLRef n) (lift (S O) d0
+y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S n) O u) (lift (S O) d0
+y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x0:
+T).(\lambda (x1: C).(\lambda (H8: (eq T u (lift (S O) (minus d0 (S n))
+x0))).(\lambda (H9: (getl n a (CHead x1 (Bind Abst) x0))).(\lambda (H10:
+(drop (S O) (minus d0 (S n)) d x1)).(let H11 \def (eq_ind T u (\lambda (t0:
+T).(\forall (e0: C).(\forall (u1: T).(\forall (d1: nat).((getl d1 d (CHead e0
+(Bind Void) u1)) \to (\forall (a0: C).((drop (S O) d1 d a0) \to (ex3_2 T T
+(\lambda (y1: T).(\lambda (_: T).(eq T t0 (lift (S O) d1 y1)))) (\lambda (_:
+T).(\lambda (y2: T).(eq T t (lift (S O) d1 y2)))) (\lambda (y1: T).(\lambda
+(y2: T).(ty3 g a0 y1 y2))))))))))) H2 (lift (S O) (minus d0 (S n)) x0) H8) in
+(let H12 \def (eq_ind T u (\lambda (t0: T).(ty3 g d t0 t)) H1 (lift (S O)
+(minus d0 (S n)) x0) H8) in (eq_ind_r T (lift (S O) (minus d0 (S n)) x0)
+(\lambda (t0: T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (TLRef n)
+(lift (S O) d0 y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S n) O
+t0) (lift (S O) d0 y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1
+y2))))) (let H13 \def (H11 e u0 (minus d0 (S n)) (getl_gen_S (Bind Abst) d
+(CHead e (Bind Void) u0) u (minus d0 (S n)) H6) x1 H10) in (ex3_2_ind T T
+(\lambda (y1: T).(\lambda (_: T).(eq T (lift (S O) (minus d0 (S n)) x0) (lift
+(S O) (minus d0 (S n)) y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T t (lift
+(S O) (minus d0 (S n)) y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g x1 y1
+y2))) (ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (TLRef n) (lift (S O)
+d0 y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S n) O (lift (S O)
+(minus d0 (S n)) x0)) (lift (S O) d0 y2)))) (\lambda (y1: T).(\lambda (y2:
+T).(ty3 g a y1 y2)))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H14: (eq T
+(lift (S O) (minus d0 (S n)) x0) (lift (S O) (minus d0 (S n)) x2))).(\lambda
+(H15: (eq T t (lift (S O) (minus d0 (S n)) x3))).(\lambda (H16: (ty3 g x1 x2
+x3)).(let H17 \def (eq_ind T t (\lambda (t0: T).(ty3 g d (lift (S O) (minus
+d0 (S n)) x0) t0)) H12 (lift (S O) (minus d0 (S n)) x3) H15) in (let H18 \def
+(eq_ind_r T x2 (\lambda (t0: T).(ty3 g x1 t0 x3)) H16 x0 (lift_inj x0 x2 (S
+O) (minus d0 (S n)) H14)) in (eq_ind T (lift (S O) (plus (S n) (minus d0 (S
+n))) (lift (S n) O x0)) (\lambda (t0: T).(ex3_2 T T (\lambda (y1: T).(\lambda