DEFINITION sn3_change()
TYPE =
       ∀b:B
         .not (eq B b Abbr)
           →∀c:C.∀v1:T.∀t:T.(sn3 (CHead c (Bind b) v1) t)→∀v2:T.(sn3 (CHead c (Bind b) v2) t)
BODY =
Show proof