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