-(lift h d t1) (\lambda (t: T).(ty3 g c t x)) (\forall (e: C).((drop h d c e)
-\to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) (\lambda (t2: T).(ty3 g
-e t1 t2))))) (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(unintro nat d
-(\lambda (n: nat).((eq T y (lift h n t1)) \to (\forall (e: C).((drop h n c e)
-\to (ex2 T (\lambda (t2: T).(pc3 c (lift h n t2) x)) (\lambda (t2: T).(ty3 g
-e t1 t2))))))) (unintro T t1 (\lambda (t: T).(\forall (x0: nat).((eq T y
-(lift h x0 t)) \to (\forall (e: C).((drop h x0 c e) \to (ex2 T (\lambda (t2:
-T).(pc3 c (lift h x0 t2) x)) (\lambda (t2: T).(ty3 g e t t2)))))))) (ty3_ind
-g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).(\forall
-(x1: nat).((eq T t (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to
-(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) t0)) (\lambda (t2: T).(ty3 g e
-x0 t2))))))))))) (\lambda (c0: C).(\lambda (t2: T).(\lambda (t: T).(\lambda
-(_: (ty3 g c0 t2 t)).(\lambda (_: ((\forall (x0: T).(\forall (x1: nat).((eq T
-t2 (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda
-(t3: T).(pc3 c0 (lift h x1 t3) t)) (\lambda (t3: T).(ty3 g e x0
-t3)))))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u
-t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1
-x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t4: T).(pc3
-c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)))))))))).(\lambda
-(H5: (pc3 c0 t3 t2)).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H6: (eq T
-u (lift h x1 x0))).(\lambda (e: C).(\lambda (H7: (drop h x1 c0 e)).(let H8
-\def (eq_ind T u (\lambda (t0: T).(\forall (x2: T).(\forall (x3: nat).((eq T
-t0 (lift h x3 x2)) \to (\forall (e0: C).((drop h x3 c0 e0) \to (ex2 T
-(\lambda (t4: T).(pc3 c0 (lift h x3 t4) t3)) (\lambda (t4: T).(ty3 g e0 x2
-t4))))))))) H4 (lift h x1 x0) H6) in (let H9 \def (eq_ind T u (\lambda (t0:
-T).(ty3 g c0 t0 t3)) H3 (lift h x1 x0) H6) in (let H10 \def (H8 x0 x1
-(refl_equal T (lift h x1 x0)) e H7) in (ex2_ind T (\lambda (t4: T).(pc3 c0
-(lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)) (ex2 T (\lambda (t4:
-T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4: T).(ty3 g e x0 t4))) (\lambda
-(x2: T).(\lambda (H11: (pc3 c0 (lift h x1 x2) t3)).(\lambda (H12: (ty3 g e x0
-x2)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4:
-T).(ty3 g e x0 t4)) x2 (pc3_t t3 c0 (lift h x1 x2) H11 t2 H5) H12))))
-H10))))))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (x0:
-T).(\lambda (x1: nat).(\lambda (H1: (eq T (TSort m) (lift h x1 x0))).(\lambda
-(e: C).(\lambda (_: (drop h x1 c0 e)).(eq_ind_r T (TSort m) (\lambda (t:
-T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (TSort (next g m))))
-(\lambda (t2: T).(ty3 g e t t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0
-(lift h x1 t2) (TSort (next g m)))) (\lambda (t2: T).(ty3 g e (TSort m) t2))
-(TSort (next g m)) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(pc3 c0 t
-(TSort (next g m)))) (pc3_refl c0 (TSort (next g m))) (lift h x1 (TSort (next
-g m))) (lift_sort (next g m) h x1)) (ty3_sort g e m)) x0 (lift_gen_sort h x1
-m x0 H1))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d0: C).(\lambda
-(u: T).(\lambda (H1: (getl n c0 (CHead d0 (Bind Abbr) u))).(\lambda (t:
-T).(\lambda (H2: (ty3 g d0 u t)).(\lambda (H3: ((\forall (x0: T).(\forall
-(x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: C).((drop h x1 d0 e) \to
-(ex2 T (\lambda (t2: T).(pc3 d0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e
-x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq T
-(TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda (H5: (drop h x1 c0
-e)).(let H_x \def (lift_gen_lref x0 x1 h n H4) in (let H6 \def H_x in (or_ind
-(land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 h) n) (eq T x0 (TLRef
-(minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O
-t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: (land (lt n x1) (eq T
-x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n)) (ex2 T (\lambda (t2:
-T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0
-t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 (TLRef n))).(eq_ind_r T
-(TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2)
-(lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind
-nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5 (S (plus n (minus x1 (S n))))
-(lt_plus_minus n x1 H8)) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
-C).(eq T u (lift h (minus x1 (S n)) v)))) (\lambda (v: T).(\lambda (e0:
-C).(getl n e (CHead e0 (Bind Abbr) v)))) (\lambda (_: T).(\lambda (e0:
-C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h
-x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda
-(x2: T).(\lambda (x3: C).(\lambda (H11: (eq T u (lift h (minus x1 (S n))
-x2))).(\lambda (H12: (getl n e (CHead x3 (Bind Abbr) x2))).(\lambda (H13:
-(drop h (minus x1 (S n)) d0 x3)).(let H14 \def (eq_ind T u (\lambda (t0:
-T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall
-(e0: C).((drop h x5 d0 e0) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x5 t2)
-t)) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H3 (lift h (minus x1 (S n)) x2)
-H11) in (let H15 \def (eq_ind T u (\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift
-h (minus x1 (S n)) x2) H11) in (let H16 \def (H14 x2 (minus x1 (S n))
-(refl_equal T (lift h (minus x1 (S n)) x2)) x3 H13) in (ex2_ind T (\lambda
-(t2: T).(pc3 d0 (lift h (minus x1 (S n)) t2) t)) (\lambda (t2: T).(ty3 g x3
-x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t)))
-(\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda (x4: T).(\lambda (H17:
-(pc3 d0 (lift h (minus x1 (S n)) x4) t)).(\lambda (H18: (ty3 g x3 x2
-x4)).(eq_ind_r nat (plus (S n) (minus x1 (S n))) (\lambda (n0: nat).(ex2 T
-(\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift (S n) O t))) (\lambda (t2:
-T).(ty3 g e (TLRef n) t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h
-(plus (S n) (minus x1 (S n))) t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g
-e (TLRef n) t2)) (lift (S n) O x4) (eq_ind_r T (lift (S n) O (lift h (minus
-x1 (S n)) x4)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O t))) (pc3_lift c0 d0
-(S n) O (getl_drop Abbr c0 d0 u n H1) (lift h (minus x1 (S n)) x4) t H17)
-(lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4)) (lift_d x4 h (S n)
-(minus x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abbr g n e x3 x2 H12 x4
-H18)) x1 (le_plus_minus (S n) x1 H8))))) H16))))))))) (getl_drop_conf_lt Abbr
-c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) H7)) (\lambda (H7: (land
-(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(and_ind (le (plus x1 h)
-n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1
-t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (le
-(plus x1 h) n)).(\lambda (H9: (eq T x0 (TLRef (minus n h)))).(eq_ind_r T
-(TLRef (minus n h)) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h
-x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 t2)))) (ex_intro2 T
+(lift h d t1) (\lambda (t: T).(ty3 g c t x)) (\lambda (_: T).(\forall (e:
+C).((drop h d c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x))
+(\lambda (t2: T).(ty3 g e t1 t2)))))) (\lambda (y: T).(\lambda (H0: (ty3 g c
+y x)).(unintro nat d (\lambda (n: nat).((eq T y (lift h n t1)) \to (\forall
+(e: C).((drop h n c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h n t2) x))
+(\lambda (t2: T).(ty3 g e t1 t2))))))) (unintro T t1 (\lambda (t: T).(\forall
+(x0: nat).((eq T y (lift h x0 t)) \to (\forall (e: C).((drop h x0 c e) \to
+(ex2 T (\lambda (t2: T).(pc3 c (lift h x0 t2) x)) (\lambda (t2: T).(ty3 g e t
+t2)))))))) (ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
+T).(\forall (x0: T).(\forall (x1: nat).((eq T t (lift h x1 x0)) \to (\forall
+(e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2)
+t0)) (\lambda (t2: T).(ty3 g e x0 t2))))))))))) (\lambda (c0: C).(\lambda
+(t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: ((\forall
+(x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (\forall (e:
+C).((drop h x1 c0 e) \to (ex2 T (\lambda (t3: T).(pc3 c0 (lift h x1 t3) t))
+(\lambda (t3: T).(ty3 g e x0 t3)))))))))).(\lambda (u: T).(\lambda (t3:
+T).(\lambda (H3: (ty3 g c0 u t3)).(\lambda (H4: ((\forall (x0: T).(\forall
+(x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to
+(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e
+x0 t4)))))))))).(\lambda (H5: (pc3 c0 t3 t2)).(\lambda (x0: T).(\lambda (x1:
+nat).(\lambda (H6: (eq T u (lift h x1 x0))).(\lambda (e: C).(\lambda (H7:
+(drop h x1 c0 e)).(let H8 \def (eq_ind T u (\lambda (t0: T).(\forall (x2:
+T).(\forall (x3: nat).((eq T t0 (lift h x3 x2)) \to (\forall (e0: C).((drop h
+x3 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x3 t4) t3)) (\lambda
+(t4: T).(ty3 g e0 x2 t4))))))))) H4 (lift h x1 x0) H6) in (let H9 \def
+(eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t3)) H3 (lift h x1 x0) H6) in (let
+H10 \def (H8 x0 x1 (refl_equal T (lift h x1 x0)) e H7) in (ex2_ind T (\lambda
+(t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)) (ex2 T
+(\lambda (t4: T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4: T).(ty3 g e x0
+t4))) (\lambda (x2: T).(\lambda (H11: (pc3 c0 (lift h x1 x2) t3)).(\lambda
+(H12: (ty3 g e x0 x2)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4)
+t2)) (\lambda (t4: T).(ty3 g e x0 t4)) x2 (pc3_t t3 c0 (lift h x1 x2) H11 t2
+H5) H12)))) H10))))))))))))))))))) (\lambda (c0: C).(\lambda (m:
+nat).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H1: (eq T (TSort m) (lift
+h x1 x0))).(\lambda (e: C).(\lambda (_: (drop h x1 c0 e)).(eq_ind_r T (TSort
+m) (\lambda (t: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (TSort
+(next g m)))) (\lambda (t2: T).(ty3 g e t t2)))) (ex_intro2 T (\lambda (t2:
+T).(pc3 c0 (lift h x1 t2) (TSort (next g m)))) (\lambda (t2: T).(ty3 g e
+(TSort m) t2)) (TSort (next g m)) (eq_ind_r T (TSort (next g m)) (\lambda (t:
+T).(pc3 c0 t (TSort (next g m)))) (pc3_refl c0 (TSort (next g m))) (lift h x1
+(TSort (next g m))) (lift_sort (next g m) h x1)) (ty3_sort g e m)) x0
+(lift_gen_sort h x1 m x0 H1))))))))) (\lambda (n: nat).(\lambda (c0:
+C).(\lambda (d0: C).(\lambda (u: T).(\lambda (H1: (getl n c0 (CHead d0 (Bind
+Abbr) u))).(\lambda (t: T).(\lambda (H2: (ty3 g d0 u t)).(\lambda (H3:
+((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1 x0)) \to (\forall
+(e: C).((drop h x1 d0 e) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x1 t2)
+t)) (\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1:
+nat).(\lambda (H4: (eq T (TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda
+(H5: (drop h x1 c0 e)).(let H_x \def (lift_gen_lref x0 x1 h n H4) in (let H6
+\def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1
+h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h
+x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7:
+(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n))
+(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda
+(t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0
+(TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2:
+T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0
+t2)))) (let H10 \def (eq_ind nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5
+(S (plus n (minus x1 (S n)))) (lt_plus_minus n x1 H8)) in (ex3_2_ind T C
+(\lambda (v: T).(\lambda (_: C).(eq T u (lift h (minus x1 (S n)) v))))
+(\lambda (v: T).(\lambda (e0: C).(getl n e (CHead e0 (Bind Abbr) v))))
+(\lambda (_: T).(\lambda (e0: C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T
+(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2:
+T).(ty3 g e (TLRef n) t2))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H11:
+(eq T u (lift h (minus x1 (S n)) x2))).(\lambda (H12: (getl n e (CHead x3
+(Bind Abbr) x2))).(\lambda (H13: (drop h (minus x1 (S n)) d0 x3)).(let H14
+\def (eq_ind T u (\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T
+t0 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 d0 e0) \to (ex2 T
+(\lambda (t2: T).(pc3 d0 (lift h x5 t2) t)) (\lambda (t2: T).(ty3 g e0 x4
+t2))))))))) H3 (lift h (minus x1 (S n)) x2) H11) in (let H15 \def (eq_ind T u
+(\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift h (minus x1 (S n)) x2) H11) in
+(let H16 \def (H14 x2 (minus x1 (S n)) (refl_equal T (lift h (minus x1 (S n))
+x2)) x3 H13) in (ex2_ind T (\lambda (t2: T).(pc3 d0 (lift h (minus x1 (S n))
+t2) t)) (\lambda (t2: T).(ty3 g x3 x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0
+(lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)))
+(\lambda (x4: T).(\lambda (H17: (pc3 d0 (lift h (minus x1 (S n)) x4)
+t)).(\lambda (H18: (ty3 g x3 x2 x4)).(eq_ind_r nat (plus (S n) (minus x1 (S
+n))) (\lambda (n0: nat).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift
+(S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)))) (ex_intro2 T (\lambda
+(t2: T).(pc3 c0 (lift h (plus (S n) (minus x1 (S n))) t2) (lift (S n) O t)))
+(\lambda (t2: T).(ty3 g e (TLRef n) t2)) (lift (S n) O x4) (eq_ind_r T (lift
+(S n) O (lift h (minus x1 (S n)) x4)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n)
+O t))) (pc3_lift c0 d0 (S n) O (getl_drop Abbr c0 d0 u n H1) (lift h (minus
+x1 (S n)) x4) t H17) (lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4))
+(lift_d x4 h (S n) (minus x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abbr g
+n e x3 x2 H12 x4 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16)))))))))
+(getl_drop_conf_lt Abbr c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9)))
+H7)) (\lambda (H7: (land (le (plus x1 h) n) (eq T x0 (TLRef (minus n
+h))))).(land_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T