DEFINITION ty3_getl_subst0()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀u:T
               .ty3 g c t u
                 →∀v0:T
                      .∀t0:T
                        .∀i:nat
                          .subst0 i v0 t t0
                            →∀b:B.∀d:C.∀v:T.(getl i c (CHead d (Bind b) v))→(ex T λw:T.ty3 g d v w)
BODY =
Show proof