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 =
        assume b: B
        assume c: C
        assume v: T
        assume t: T
        suppose H: sn3 c (THead (Bind b) v t)
          (H_x) 
             by (sn3_gen_bind . . . . H)
land (sn3 c v) (sn3 (CHead c (Bind b) v) t)
          end of H_x
          (H0) consider H_x
          we proceed by induction on H0 to prove sn3 (CHead c (Bind b) v) t
             case conj : :sn3 c v H2:sn3 (CHead c (Bind b) v) t ⇒
                the thesis becomes the hypothesis H2
          we proved sn3 (CHead c (Bind b) v) t
       we proved 
          ∀b:B
            .∀c:C.∀v:T.∀t:T.(sn3 c (THead (Bind b) v t))→(sn3 (CHead c (Bind b) v) t)