DEFINITION pr3_pr1()
TYPE =
       ∀t1:T.∀t2:T.(pr1 t1 t2)→∀c:C.(pr3 c t1 t2)
BODY =
        assume t1: T
        assume t2: T
        suppose H: pr1 t1 t2
          we proceed by induction on H to prove ∀c:C.(pr3 c t1 t2)
             case pr1_refl : t:T ⇒
                the thesis becomes ∀c:C.(pr3 c t t)
                   assume c: C
                      by (pr3_refl . .)
                      we proved pr3 c t t
∀c:C.(pr3 c t t)
             case pr1_sing : t0:T t3:T H0:pr0 t3 t0 t4:T :pr1 t0 t4 ⇒
                the thesis becomes ∀c:C.(pr3 c t3 t4)
                (H2) by induction hypothesis we know ∀c:C.(pr3 c t0 t4)
                   assume c: C
                      (h1) 
                         by (pr2_free . . . H0)
pr2 c t3 t0
                      end of h1
                      (h2) by (H2 .) we proved pr3 c t0 t4
                      by (pr3_sing . . . h1 . h2)
                      we proved pr3 c t3 t4
∀c:C.(pr3 c t3 t4)
          we proved ∀c:C.(pr3 c t1 t2)
       we proved ∀t1:T.∀t2:T.(pr1 t1 t2)→∀c:C.(pr3 c t1 t2)