DEFINITION ty3_sn3()
TYPE =
∀
g:
G
.
∀
c:
C
.
∀
t:
T
.
∀
u:
T
.(
ty3
g c t u)
→
(
sn3
c t)
BODY =
Show proof