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