DEFINITION pc3_fsubst0()
TYPE =
       ∀c1:C
         .∀t1:T
           .∀t:T
             .pc3 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))→(pc3 c2 t2 t)
BODY =
Show proof