DEFINITION pc1_pr0_r()
TYPE =
       ∀t1:T.∀t2:T.(pr0 t1 t2)→(pc1 t1 t2)
BODY =
Show proof