-(lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S (S n) i H0))))
-(\lambda (H0: (eq nat n i)).(let H1 \def (eq_ind_r nat i (\lambda (n0:
-nat).(le h n0)) H n H0) in (eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef
-h) (lift (S h) (S n0) (TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T
-(TLRef n) (\lambda (t: T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n))))
-(eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef
-n) t)) (eq_ind nat (S (plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h)
-(TLRef n) (TLRef n0))) (eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n
-(TLRef h) (TLRef n) (TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0:
-nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O
-(TLRef h)) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n
-(TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n))
-(TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n))
-(sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h)
-(plus_sym n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n))
-(lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt
-n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T
-(TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i
-(TLRef n)))) (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i
-(TLRef h) (TLRef (plus n (S h))) t)) (subst1_refl i (TLRef h) (TLRef (plus n
-(S h)))) (lift (S h) i (TLRef n)) (lift_lref_ge n (S h) i (le_S_n i n (le_S
-(S i) n H0)))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h) (S i)
-H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i:
+(lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S_n (S n) (S i)
+(le_S (S (S n)) (S i) (le_n_S (S n) i H0)))))) (\lambda (H0: (eq nat n
+i)).(let H1 \def (eq_ind_r nat i (\lambda (n0: nat).(le h n0)) H n H0) in
+(eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef h) (lift (S h) (S n0)
+(TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T (TLRef n) (\lambda (t:
+T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n)))) (eq_ind_r T (TLRef (plus
+n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (eq_ind nat (S
+(plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0)))
+(eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n (TLRef h) (TLRef n)
+(TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0: nat).(subst1 n
+(TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O (TLRef h)) (\lambda
+(t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n (TLRef h) (TLRef n)
+(lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) (TLRef (plus h (S n)))
+(lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) (sym_eq nat (S (plus h
+n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) (plus_sym n h)) (plus n (S
+h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) (lift_lref_ge n (S h) n (le_n
+n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt n (S h) (S n) (le_n (S n))))
+i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T (TLRef (plus n (S h))) (\lambda
+(t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T (TLRef
+(plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) (TLRef (plus n (S h)))
+t)) (subst1_refl i (TLRef h) (TLRef (plus n (S h)))) (lift (S h) i (TLRef n))
+(lift_lref_ge n (S h) i (le_S_n i n (le_S_n (S i) (S n) (le_S (S (S i)) (S n)
+(le_n_S (S i) n H0)))))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h)
+(S i) H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i: