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