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