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