DEFINITION ty3_subst0()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀t:T
               .ty3 g c t1 t
                 →∀e:C
                      .∀u:T
                        .∀i:nat
                          .(getl i c (CHead e (Bind Abbr) u))→∀t2:T.(subst0 i u t1 t2)→(ty3 g c t2 t)
BODY =
Show proof