DEFINITION ty3_acyclic()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀u:T.(ty3 g c t u)→(pc3 c u t)→∀P:Prop.P
BODY =
Show proof