-(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0)
-with [refl_equal \Rightarrow H])))))).
+(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(let TMP_1 \def (sym_eq
+A y x H0) in (match TMP_1 with [refl_equal \Rightarrow H]))))))).