DEFINITION ty3_sred_pr2()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 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: pr2 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 pr2_free : c0:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes ∀g:G.∀t:T.∀H1:(ty3 g c0 t3 t).(ty3 g c0 t4 t)
                    assume g: G
                    assume t: T
                    suppose H1: ty3 g c0 t3 t
                      by (wcpr0_refl .)
                      we proved wcpr0 c0 c0
                      by (ty3_sred_wcpr0_pr0 . . . . H1 . previous . H0)
                      we proved ty3 g c0 t4 t
∀g:G.∀t:T.∀H1:(ty3 g c0 t3 t).(ty3 g c0 t4 t)
             case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H1:pr0 t3 t4 t:T H2:subst0 i u t4 t ⇒
                the thesis becomes ∀g:G.∀t0:T.∀H3:(ty3 g c0 t3 t0).(ty3 g c0 t t0)
                    assume g: G
                    assume t0: T
                    suppose H3: ty3 g c0 t3 t0
                      by (wcpr0_refl .)
                      we proved wcpr0 c0 c0
                      by (ty3_sred_wcpr0_pr0 . . . . H3 . previous . H1)
                      we proved ty3 g c0 t4 t0
                      by (ty3_subst0 . . . . previous . . . H0 . H2)
                      we proved ty3 g c0 t t0
∀g:G.∀t0:T.∀H3:(ty3 g c0 t3 t0).(ty3 g c0 t t0)
          we proved ∀g:G.∀t3:T.(ty3 g c t1 t3)→(ty3 g c t2 t3)
       we proved ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→∀g:G.∀t3:T.(ty3 g c t1 t3)→(ty3 g c t2 t3)