DEFINITION sn3_appl_bind()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀c:C
                .∀u:T
                  .sn3 c u
                    →∀t:T
                         .∀v:T
                           .sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t)
                             →sn3 c (THead (Flat Appl) v (THead (Bind b) u t))
BODY =
Show proof