-(plus n h)) (TLRef n)) H (lt_le_S n d (le_lt_trans n (plus n h) d (le_plus_l
-n h) H5)))) n0 H4)))]) in (H3 (refl_equal T (TLRef n0)))))) (\lambda (H1: (le
-d n0)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t0: T).(eq T
-(TLRef (plus n h)) t0)) H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in
-(let H3 \def (match H2 in eq return (\lambda (t0: T).(\lambda (_: (eq ? ?
-t0)).((eq T t0 (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TLRef n))))) with
-[refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef (plus n h)) (TLRef (plus
-n0 h)))).(let H4 \def (f_equal T nat (\lambda (e: T).(match e in T return
-(\lambda (_: T).nat) with [(TSort _) \Rightarrow ((let rec plus (n1: nat) on
-n1: (nat \to nat) \def (\lambda (m: nat).(match n1 with [O \Rightarrow m | (S
-p) \Rightarrow (S (plus p m))])) in plus) n h) | (TLRef n1) \Rightarrow n1 |
-(THead _ _ _) \Rightarrow ((let rec plus (n1: nat) on n1: (nat \to nat) \def
-(\lambda (m: nat).(match n1 with [O \Rightarrow m | (S p) \Rightarrow (S
-(plus p m))])) in plus) n h)])) (TLRef (plus n h)) (TLRef (plus n0 h)) H3) in
-(eq_ind nat (plus n h) (\lambda (_: nat).(eq T (TLRef n0) (TLRef n)))
-(f_equal nat T TLRef n0 n (simpl_plus_r h n0 n (sym_eq nat (plus n h) (plus
-n0 h) H4))) (plus n0 h) H4)))]) in (H3 (refl_equal T (TLRef (plus n0
-h)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TLRef
-(plus n h)) (lift h d t0)) \to (eq T t0 (TLRef n))))).(\lambda (t1:
-T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d t1)) \to (eq T t1 (TLRef
-n))))).(\lambda (H2: (eq T (TLRef (plus n h)) (lift h d (THead k t0
-t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t2: T).(eq
-T (TLRef (plus n h)) t2)) H2 (THead k (lift h d t0) (lift h (s k d) t1))
-(lift_head k t0 t1 h d)) in (let H4 \def (match H3 in eq return (\lambda (t2:
-T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h d t0) (lift h (s k d)
-t1))) \to (eq T (THead k t0 t1) (TLRef n))))) with [refl_equal \Rightarrow
-(\lambda (H4: (eq T (TLRef (plus n h)) (THead k (lift h d t0) (lift h (s k d)
-t1)))).(let H5 \def (eq_ind T (TLRef (plus n h)) (\lambda (e: T).(match e in
-T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d
-t0) (lift h (s k d) t1)) H4) in (False_ind (eq T (THead k t0 t1) (TLRef n))
-H5)))]) in (H4 (refl_equal T (THead k (lift h d t0) (lift h (s k d)
-t1)))))))))))) t))))).
+(plus n h)) (TLRef n)) H (lt_le_S n d (simpl_lt_plus_r h n d (lt_le_trans
+(plus n h) d (plus d h) H5 (le_plus_l d h)))))) n0 H4)))]) in (H3 (refl_equal
+T (TLRef n0)))))) (\lambda (H1: (le d n0)).(let H2 \def (eq_ind T (lift h d
+(TLRef n0)) (\lambda (t0: T).(eq T (TLRef (plus n h)) t0)) H0 (TLRef (plus n0
+h)) (lift_lref_ge n0 h d H1)) in (let H3 \def (match H2 in eq return (\lambda
+(t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n0 h))) \to (eq T
+(TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H3: (eq T
+(TLRef (plus n h)) (TLRef (plus n0 h)))).(let H4 \def (f_equal T nat (\lambda
+(e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow
+((let rec plus (n1: nat) on n1: (nat \to nat) \def (\lambda (m: nat).(match
+n1 with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)
+| (TLRef n1) \Rightarrow n1 | (THead _ _ _) \Rightarrow ((let rec plus (n1:
+nat) on n1: (nat \to nat) \def (\lambda (m: nat).(match n1 with [O
+\Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef
+(plus n h)) (TLRef (plus n0 h)) H3) in (eq_ind nat (plus n h) (\lambda (_:
+nat).(eq T (TLRef n0) (TLRef n))) (f_equal nat T TLRef n0 n (simpl_plus_r h
+n0 n (sym_eq nat (plus n h) (plus n0 h) H4))) (plus n0 h) H4)))]) in (H3
+(refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0:
+T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d t0)) \to (eq T t0 (TLRef
+n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d
+t1)) \to (eq T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef (plus n h)) (lift
+h d (THead k t0 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1))
+(\lambda (t2: T).(eq T (TLRef (plus n h)) t2)) H2 (THead k (lift h d t0)
+(lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H4 \def (match H3 in eq
+return (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h
+d t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TLRef n))))) with
+[refl_equal \Rightarrow (\lambda (H4: (eq T (TLRef (plus n h)) (THead k (lift
+h d t0) (lift h (s k d) t1)))).(let H5 \def (eq_ind T (TLRef (plus n h))
+(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
+\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
+False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H4) in (False_ind (eq
+T (THead k t0 t1) (TLRef n)) H5)))]) in (H4 (refl_equal T (THead k (lift h d
+t0) (lift h (s k d) t1)))))))))))) t))))).