\forall (A: Type[0]).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall
(x: A).(P x))) \to (P a))))
\def
\lambda (A: Type[0]).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda
(H: ((\forall (x: A).(P x)))).(H a)))).
\forall (A: Type[0]).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall
(x: A).(P x))) \to (P a))))
\def
\lambda (A: Type[0]).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda
(H: ((\forall (x: A).(P x)))).(H a)))).