DEFINITION sn3_appls_bind()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀c:C
                .∀u:T
                  .sn3 c u
                    →∀vs:TList
                         .∀t:T
                           .(sn3
                               CHead c (Bind b) u
                               THeads (Flat Appl) (lifts (S O) O vs) t)
                             →sn3 c (THeads (Flat Appl) vs (THead (Bind b) u t))
BODY =
Show proof