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