DEFINITION pc3_refl()
TYPE =
∀
c:
C
.
∀
t:
T
.(
pc3
c t t)
BODY =
Show proof