DEFINITION pc3_s()
TYPE =
∀
c:
C
.
∀
t2:
T
.
∀
t1:
T
.(
pc3
c t1 t2)
→
(
pc3
c t2 t1)
BODY =
Show proof