DEFINITION sn3_shift()
TYPE =
       ∀b:B
         .∀c:C.∀v:T.∀t:T.(sn3 c (THead (Bind b) v t))→(sn3 (CHead c (Bind b) v) t)
BODY =
Show proof