DEFINITION pr1_t()
TYPE =
       ∀t2:T.∀t1:T.(pr1 t1 t2)→∀t3:T.(pr1 t2 t3)→(pr1 t1 t3)
BODY =
        assume t2: T
        assume t1: T
        suppose H: pr1 t1 t2
          we proceed by induction on H to prove ∀t3:T.(pr1 t2 t3)→(pr1 t1 t3)
             case pr1_refl : t:T ⇒
                    assume t3: T
                    suppose H0: pr1 t t3
                      consider H0
             case pr1_sing : t0:T t3:T H0:pr0 t3 t0 t4:T :pr1 t0 t4 ⇒
                the thesis becomes ∀t5:T.∀H3:(pr1 t4 t5).(pr1 t3 t5)
                (H2) by induction hypothesis we know ∀t5:T.(pr1 t4 t5)→(pr1 t0 t5)
                    assume t5: T
                    suppose H3: pr1 t4 t5
                      by (H2 . H3)
                      we proved pr1 t0 t5
                      by (pr1_sing . . H0 . previous)
                      we proved pr1 t3 t5
∀t5:T.∀H3:(pr1 t4 t5).(pr1 t3 t5)
          we proved ∀t3:T.(pr1 t2 t3)→(pr1 t1 t3)
       we proved ∀t2:T.∀t1:T.(pr1 t1 t2)→∀t3:T.(pr1 t2 t3)→(pr1 t1 t3)