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