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