-H9 H6 H7))) | (pr0_epsilon t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T
-(THead (Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6
-t4)).((let H9 \def (eq_ind T (THead (Flat Cast) u0 t5) (\lambda (e: T).(match
-e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
+H9 H6 H7))) | (pr0_tau t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T (THead
+(Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6 t4)).((let
+H9 \def (eq_ind T (THead (Flat Cast) u0 t5) (\lambda (e: T).(match e in T
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
+(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow