DEFINITION ty3_sred_back()
TYPE =
       ∀g:G.∀c:C.∀t1:T.∀t0:T.(ty3 g c t1 t0)→∀t2:T.(pr3 c t1 t2)→∀t:T.(ty3 g c t2 t)→(ty3 g c t1 t)
BODY =
        assume g: G
        assume c: C
        assume t1: T
        assume t0: T
        suppose H: ty3 g c t1 t0
        assume t2: T
        suppose H0: pr3 c t1 t2
        assume t: T
        suppose H1: ty3 g c t2 t
          by (ty3_correct . . . . H1)
          we proved ex T λt:T.ty3 g c t t
          we proceed by induction on the previous result to prove ty3 g c t1 t
             case ex_intro : x:T H2:ty3 g c t x ⇒
                the thesis becomes ty3 g c t1 t
                   by (ty3_sred_pr3 . . . H0 . . H)
                   we proved ty3 g c t2 t0
                   by (ty3_unique . . . . previous . H1)
                   we proved pc3 c t0 t
                   by (ty3_conv . . . . H2 . . H previous)
ty3 g c t1 t
          we proved ty3 g c t1 t
       we proved ∀g:G.∀c:C.∀t1:T.∀t0:T.(ty3 g c t1 t0)→∀t2:T.(pr3 c t1 t2)→∀t:T.(ty3 g c t2 t)→(ty3 g c t1 t)