-[(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t _)
-\Rightarrow t])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1) H1)
-in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda
-(_: T).T) with [(TSort _) \Rightarrow (THead k0 ((let rec lref_map (f: ((nat
-\to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow
-(TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true
-\Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow
-(THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda
-(x: nat).(plus x h)) d t0) ((let rec lref_map (f: ((nat \to nat))) (d: nat)
-(t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef
-i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false
-\Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u)
-(lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) (s k0
-d) t1)) | (TLRef _) \Rightarrow (THead k0 ((let rec lref_map (f: ((nat \to
-nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow
-(TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true
-\Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow
-(THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda
-(x: nat).(plus x h)) d t0) ((let rec lref_map (f: ((nat \to nat))) (d: nat)
-(t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef
-i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false
-\Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u)
-(lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) (s k0
-d) t1)) | (THead _ _ t) \Rightarrow t])) (THead k v (lift h d (THead k0 t0
-t1))) (THead k0 t0 t1) H1) in (\lambda (_: (eq T v t0)).(\lambda (H6: (eq K k
-k0)).(let H7 \def (eq_ind K k (\lambda (k: K).(\forall (v: T).(\forall (h:
-nat).(\forall (d: nat).((eq T (THead k v (lift h d t1)) t1) \to (\forall (P:
-Prop).P)))))) H0 k0 H6) in (let H8 \def (eq_ind T (lift h d (THead k0 t0 t1))
-(\lambda (t: T).(eq T t t1)) H4 (THead k0 (lift h d t0) (lift h (s k0 d) t1))
-(lift_head k0 t0 t1 h d)) in (H7 (lift h d t0) h (s k0 d) H8 P)))))) H3))
-H2)))))))))))) t)).
+[(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t2 _)
+\Rightarrow t2])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1)
+H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
+(\lambda (_: T).T) with [(TSort _) \Rightarrow (THead k0 ((let rec lref_map
+(f: ((nat \to nat))) (d0: nat) (t2: T) on t2: T \def (match t2 with [(TSort
+n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0)
+with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k1 u t3)
+\Rightarrow (THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3))]) in
+lref_map) (\lambda (x: nat).(plus x h)) d t0) ((let rec lref_map (f: ((nat
+\to nat))) (d0: nat) (t2: T) on t2: T \def (match t2 with [(TSort n)
+\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0) with
+[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k1 u t3)
+\Rightarrow (THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3))]) in
+lref_map) (\lambda (x: nat).(plus x h)) (s k0 d) t1)) | (TLRef _) \Rightarrow
+(THead k0 ((let rec lref_map (f: ((nat \to nat))) (d0: nat) (t2: T) on t2: T
+\def (match t2 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow
+(TLRef (match (blt i d0) with [true \Rightarrow i | false \Rightarrow (f
+i)])) | (THead k1 u t3) \Rightarrow (THead k1 (lref_map f d0 u) (lref_map f
+(s k1 d0) t3))]) in lref_map) (\lambda (x: nat).(plus x h)) d t0) ((let rec
+lref_map (f: ((nat \to nat))) (d0: nat) (t2: T) on t2: T \def (match t2 with
+[(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i
+d0) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k1 u t3)
+\Rightarrow (THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3))]) in
+lref_map) (\lambda (x: nat).(plus x h)) (s k0 d) t1)) | (THead _ _ t2)
+\Rightarrow t2])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1)
+H1) in (\lambda (_: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let H7 \def
+(eq_ind K k (\lambda (k1: K).(\forall (v0: T).(\forall (h0: nat).(\forall
+(d0: nat).((eq T (THead k1 v0 (lift h0 d0 t1)) t1) \to (\forall (P0:
+Prop).P0)))))) H0 k0 H6) in (let H8 \def (eq_ind T (lift h d (THead k0 t0
+t1)) (\lambda (t2: T).(eq T t2 t1)) H4 (THead k0 (lift h d t0) (lift h (s k0
+d) t1)) (lift_head k0 t0 t1 h d)) in (H7 (lift h d t0) h (s k0 d) H8 P))))))
+H3)) H2)))))))))))) t)).