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