-(lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (plus_lt_compat_r n d2 h1 H3) x
-H2))) (\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2:
-T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2
-t2)))) (\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2
-h1) (plus n h1) (plus_le_compat d2 n h1 h1 H3 (le_n h1)) (eq_ind_r nat (plus
-(plus d2 h2) h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (plus_lt_compat_r n
-(plus d2 h2) h1 H4) (plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x
-H2 (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T
-(TLRef n) (lift h2 d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5
-\def (eq_ind nat (plus n h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2
-(plus d2 h1) x))) H2 (plus (minus (plus n h1) h2) h2) (le_plus_minus_sym h2
-(plus n h1) (le_plus_trans h2 n h1 (le_trans h2 (plus d2 h2) n (le_plus_r d2
-h2) H4)))) in (eq_ind_r T (TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2
-T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n)
-(lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n
-h1) h2)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))
-(TLRef (minus n h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0:
-nat).(eq T (TLRef n0) (lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef
-(plus (minus n h2) h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1))
-t)) (refl_equal T (TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n
-h2))) (lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H
-(le_minus d2 n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans
-h2 (plus d2 h2) n (le_plus_r d2 h2) H4) h1)) (eq_ind_r nat (plus (minus n h2)
-h2) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2)))))
+(lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (lt_reg_r n d2 h1 H3) x H2)))
+(\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2: T).(eq
+T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))))
+(\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2 h1) (plus
+n h1) (le_plus_plus d2 n h1 h1 H3 (le_n h1)) (eq_ind_r nat (plus (plus d2 h2)
+h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (lt_reg_r n (plus d2 h2) h1 H4)
+(plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x H2 (ex2 T (\lambda
+(t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2
+d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5 \def (eq_ind nat (plus
+n h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 (plus d2 h1) x))) H2 (plus
+(minus (plus n h1) h2) h2) (le_plus_minus_sym h2 (plus n h1) (le_plus_trans
+h2 n h1 (le_trans h2 (plus d2 h2) n (le_plus_r d2 h2) H4)))) in (eq_ind_r T
+(TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T
+t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))))
+(ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n h1) h2)) (lift h1
+d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) (TLRef (minus n
+h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0: nat).(eq T (TLRef n0)
+(lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef (plus (minus n h2)
+h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1)) t)) (refl_equal T
+(TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n h2)))
+(lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H (le_minus d2
+n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans h2 (plus d2
+h2) n (le_plus_r d2 h2) H4) h1)) (eq_ind_r nat (plus (minus n h2) h2)
+(\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2)))))