DEFINITION unintro()
TYPE =
∀
A:
Set
.
∀
a:A.
∀
P:A
→
Prop
.(
∀
x:A.(P x))
→
(P a)
BODY =
Show proof