DEFINITION pc3_dec()
TYPE =
       ∀g:G.∀c:C.∀u1:T.∀t1:T.(ty3 g c u1 t1)→∀u2:T.∀t2:T.(ty3 g c u2 t2)→(or (pc3 c u1 u2) (pc3 c u1 u2)→False)
BODY =
Show proof