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