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