DEFINITION pr2_change()
TYPE =
       ∀b:B
         .not (eq B b Abbr)
           →∀c:C.∀v1:T.∀t1:T.∀t2:T.(pr2 (CHead c (Bind b) v1) t1 t2)→∀v2:T.(pr2 (CHead c (Bind b) v2) t1 t2)
BODY =
Show proof