-(THead k0 t0 t1))).(\lambda (P: Prop).(let TMP_12 \def (\lambda (e: T).(match
-e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k1 _ _)
-\Rightarrow k1])) in (let TMP_13 \def (THead k0 t0 t1) in (let TMP_14 \def
-(THead k v TMP_13) in (let TMP_15 \def (THead k0 t0 t1) in (let H2 \def
-(f_equal T K TMP_12 TMP_14 TMP_15 H1) in (let TMP_16 \def (\lambda (e:
-T).(match e with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead
-_ t2 _) \Rightarrow t2])) in (let TMP_17 \def (THead k0 t0 t1) in (let TMP_18
-\def (THead k v TMP_17) in (let TMP_19 \def (THead k0 t0 t1) in (let H3 \def
-(f_equal T T TMP_16 TMP_18 TMP_19 H1) in (let TMP_20 \def (\lambda (e:
-T).(match e with [(TSort _) \Rightarrow (THead k0 t0 t1) | (TLRef _)
-\Rightarrow (THead k0 t0 t1) | (THead _ _ t2) \Rightarrow t2])) in (let
-TMP_21 \def (THead k0 t0 t1) in (let TMP_22 \def (THead k v TMP_21) in (let
-TMP_23 \def (THead k0 t0 t1) in (let H4 \def (f_equal T T TMP_20 TMP_22
-TMP_23 H1) in (let TMP_26 \def (\lambda (H5: (eq T v t0)).(\lambda (H6: (eq K
-k k0)).(let TMP_24 \def (\lambda (t2: T).((eq T (THead k t2 t1) t1) \to
-(\forall (P0: Prop).P0))) in (let H7 \def (eq_ind T v TMP_24 H0 t0 H5) in
-(let TMP_25 \def (\lambda (k1: K).((eq T (THead k1 t0 t1) t1) \to (\forall
-(P0: Prop).P0))) in (let H8 \def (eq_ind K k TMP_25 H7 k0 H6) in (H8 H4
-P))))))) in (let TMP_27 \def (TMP_26 H3) in (TMP_27
-H2))))))))))))))))))))))))) in (T_ind TMP_1 TMP_6 TMP_11 TMP_28 t))))))).
+(THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e:
+T).(match e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead
+k1 _ _) \Rightarrow k1])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1)
+in ((let H3 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
+\Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t2 _) \Rightarrow t2]))
+(THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T
+T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead k0 t0 t1) |
+(TLRef _) \Rightarrow (THead k0 t0 t1) | (THead _ _ t2) \Rightarrow t2]))
+(THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in (\lambda (H5: (eq T v
+t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind T v (\lambda (t2:
+T).((eq T (THead k t2 t1) t1) \to (\forall (P0: Prop).P0))) H0 t0 H5) in (let
+H8 \def (eq_ind K k (\lambda (k1: K).((eq T (THead k1 t0 t1) t1) \to (\forall
+(P0: Prop).P0))) H7 k0 H6) in (H8 H4 P)))))) H3)) H2))))))))) t))).