DEFINITION pr2_subst1()
TYPE =
       ∀c:C
         .∀e:C
           .∀v:T
             .∀i:nat
               .getl i c (CHead e (Bind Abbr) v)
                 →∀t1:T.∀t2:T.(pr2 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t2 w2)
BODY =
Show proof