-Prop).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to
-G))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
+((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to (G
+y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).