DEFINITION ty3_sred_pr0()
TYPE =
       ∀t1:T.∀t2:T.(pr0 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: pr0 t1 t2
        assume g: G
        assume c: C
        assume t: T
        suppose H0: ty3 g c t1 t
          by (wcpr0_refl .)
          we proved wcpr0 c c
          by (ty3_sred_wcpr0_pr0 . . . . H0 . previous . H)
          we proved ty3 g c t2 t
       we proved ∀t1:T.∀t2:T.(pr0 t1 t2)→∀g:G.∀c:C.∀t:T.(ty3 g c t1 t)→(ty3 g c t2 t)