\forall (S: Type[0]).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall
(G: ((S \to Prop))).(((\forall (y: S).((P y) \to ((eq S y x) \to (G y)))))
\to ((P x) \to (G x))))))
\def
\lambda (S: Type[0]).(\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
\forall (S: Type[0]).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall
(G: ((S \to Prop))).(((\forall (y: S).((P y) \to ((eq S y x) \to (G y)))))
\to ((P x) \to (G x))))))
\def
\lambda (S: Type[0]).(\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