DEFINITION sty1_appl()
TYPE =
       ∀g:G
         .∀c:C
           .∀v:T
             .∀t1:T
               .∀t2:T
                 .(sty1 g c t1 t2)→(sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t2))
BODY =
Show proof