DEFINITION ty3_csubst0()
TYPE =
       ∀g:G
         .∀c1:C
           .∀t1:T
             .∀t2:T
               .ty3 g c1 t1 t2
                 →∀e:C
                      .∀u:T.∀i:nat.(getl i c1 (CHead e (Bind Abbr) u))→∀c2:C.(csubst0 i u c1 c2)→(ty3 g c2 t1 t2)
BODY =
        assume g: G
        assume c1: C
        assume t1: T
        assume t2: T
        suppose H: ty3 g c1 t1 t2
        assume e: C
        assume u: T
        assume i: nat
        suppose H0: getl i c1 (CHead e (Bind Abbr) u)
        assume c2: C
        suppose H1: csubst0 i u c1 c2
          by (fsubst0_fst . . . . . H1)
          we proved fsubst0 i u c1 t1 c2 t1
          by (ty3_fsubst0 . . . . H . . . . previous . H0)
          we proved ty3 g c2 t1 t2
       we proved 
          ∀g:G
            .∀c1:C
              .∀t1:T
                .∀t2:T
                  .ty3 g c1 t1 t2
                    →∀e:C
                         .∀u:T.∀i:nat.(getl i c1 (CHead e (Bind Abbr) u))→∀c2:C.(csubst0 i u c1 c2)→(ty3 g c2 t1 t2)