-[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k _ _)
-\Rightarrow k])) (THead k0 v0 t0) (THead k v2 t4) H0) in (eq_ind K k (\lambda
-(k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t4) t5) \to
-(iso (THead k v1 t3) t5))))) (\lambda (H5: (eq T v0 v2)).(eq_ind T v2
-(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t4) t5) \to (iso (THead
-k v1 t3) t5)))) (\lambda (H6: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq
-T (THead k v3 t4) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H7: (eq T
-(THead k v3 t4) t5)).(eq_ind T (THead k v3 t4) (\lambda (t: T).(iso (THead k
-v1 t3) t)) (iso_head k v1 v3 t3 t4) t5 H7)) t0 (sym_eq T t0 t4 H6))) v0
-(sym_eq T v0 v2 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H1
+[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _ _)
+\Rightarrow k1])) (THead k0 v0 t0) (THead k v2 t4) H1) in (eq_ind K k
+(\lambda (k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t6)
+t5) \to (iso (THead k v1 t3) t5))))) (\lambda (H6: (eq T v0 v2)).(eq_ind T v2
+(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t6) t5) \to (iso (THead
+k v1 t3) t5)))) (\lambda (H7: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq
+T (THead k v3 t6) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H8: (eq T
+(THead k v3 t6) t5)).(eq_ind T (THead k v3 t6) (\lambda (t: T).(iso (THead k
+v1 t3) t)) (iso_head k v1 v3 t3 t6) t5 H8)) t0 (sym_eq T t0 t4 H7))) v0
+(sym_eq T v0 v2 H6))) k0 (sym_eq K k0 k H5))) H4)) H3)) H2)))]) in (H1