DEFINITION pr3_t()
TYPE =
       ∀t2:T.∀t1:T.∀c:C.(pr3 c t1 t2)→∀t3:T.(pr3 c t2 t3)→(pr3 c t1 t3)
BODY =
        assume t2: T
        assume t1: T
        assume c: C
        suppose H: pr3 c t1 t2
          we proceed by induction on H to prove ∀t3:T.(pr3 c t2 t3)→(pr3 c t1 t3)
             case pr3_refl : t:T ⇒
                    assume t3: T
                    suppose H0: pr3 c t t3
                      consider H0
             case pr3_sing : t0:T t3:T H0:pr2 c t3 t0 t4:T :pr3 c t0 t4 ⇒
                the thesis becomes ∀t5:T.∀H3:(pr3 c t4 t5).(pr3 c t3 t5)
                (H2) by induction hypothesis we know ∀t5:T.(pr3 c t4 t5)→(pr3 c t0 t5)
                    assume t5: T
                    suppose H3: pr3 c t4 t5
                      by (H2 . H3)
                      we proved pr3 c t0 t5
                      by (pr3_sing . . . H0 . previous)
                      we proved pr3 c t3 t5
∀t5:T.∀H3:(pr3 c t4 t5).(pr3 c t3 t5)
          we proved ∀t3:T.(pr3 c t2 t3)→(pr3 c t1 t3)
       we proved ∀t2:T.∀t1:T.∀c:C.(pr3 c t1 t2)→∀t3:T.(pr3 c t2 t3)→(pr3 c t1 t3)