DEFINITION ty3_unique()
TYPE =
       ∀g:G.∀c:C.∀u:T.∀t1:T.(ty3 g c u t1)→∀t2:T.(ty3 g c u t2)→(pc3 c t1 t2)
BODY =
Show proof