DEFINITION sty0_gen_appl()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀t1:T
               .∀x:T
                 .sty0 g c (THead (Flat Appl) u t1) x
                   →ex2 T λt2:T.sty0 g c t1 t2 λt2:T.eq T x (THead (Flat Appl) u t2)
BODY =
Show proof