DEFINITION pc3_refl()
TYPE =
       ∀c:C.∀t:T.(pc3 c t t)
BODY =
        assume c: C
        assume t: T
          (h1) 
             by (pr3_refl . .)
pr3 c t t
          end of h1
          (h2) 
             by (pr3_refl . .)
pr3 c t t
          end of h2
          by (ex_intro2 . . . . h1 h2)
          we proved ex2 T λt0:T.pr3 c t t0 λt0:T.pr3 c t t0
          that is equivalent to pc3 c t t
       we proved ∀c:C.∀t:T.(pc3 c t t)