\lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G:
((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))))))).
\lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G:
((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))))))).