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 =
Show proof