DEFINITION pr1_pr0()
TYPE =
       ∀t1:T.∀t2:T.(pr0 t1 t2)→(pr1 t1 t2)
BODY =
        assume t1: T
        assume t2: T
        suppose H: pr0 t1 t2
          by (pr1_refl .)
          we proved pr1 t2 t2
          by (pr1_sing . . H . previous)
          we proved pr1 t1 t2
       we proved ∀t1:T.∀t2:T.(pr0 t1 t2)→(pr1 t1 t2)