DEFINITION sn3_appls_beta()
TYPE =
       ∀c:C
         .∀v:T
           .∀t:T
             .∀us:TList
               .sn3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t))
                 →∀w:T
                      .sn3 c w
                        →(sn3
                             c
                             THeads
                               Flat Appl
                               us
                               THead (Flat Appl) v (THead (Bind Abst) w t))
BODY =
Show proof