DEFINITION pc1_refl()
TYPE =
       ∀t:T.(pc1 t t)
BODY =
       assume t: T
          (h1) by (pr1_refl .) we proved pr1 t t
          (h2) by (pr1_refl .) we proved pr1 t t
          by (ex_intro2 . . . . h1 h2)
          we proved ex2 T λt0:T.pr1 t t0 λt0:T.pr1 t t0
          that is equivalent to pc1 t t
       we proved ∀t:T.(pc1 t t)