DEFINITION xinduction()
TYPE =
∀
A:
Set
.
∀
t:A.
∀
P:A
→
Prop
.(
∀
x:A.(
eq
A t x)
→
(P x))
→
(P t)
BODY =
Show proof