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 =
        assume c: C
        assume t: T
        assume t1: T
        suppose H: pc3 c t t1
        assume t2: T
        suppose H0: pr3 c t t2
          by (pc3_pr3_x . . . H0)
          we proved pc3 c t2 t
          by (pc3_t . . . previous . H)
          we proved pc3 c t2 t1
       we proved ∀c:C.∀t:T.∀t1:T.(pc3 c t t1)→∀t2:T.(pr3 c t t2)→(pc3 c t2 t1)