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 =
        assume g: G
        assume c: C
        assume v: T
        assume t1: T
        assume t2: T
        suppose H: sty1 g c t1 t2
          we proceed by induction on H to prove sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t2)
             case sty1_sty0 : t3:T H0:sty0 g c t1 t3 ⇒
                the thesis becomes sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t3)
                   by (sty0_appl . . . . . H0)
                   we proved sty0 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t3)
                   by (sty1_sty0 . . . . previous)
sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t3)
             case sty1_sing : t:T :sty1 g c t1 t t3:T H2:sty0 g c t t3 ⇒
                the thesis becomes sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t3)
                (H1) by induction hypothesis we know sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t)
                   by (sty0_appl . . . . . H2)
                   we proved sty0 g c (THead (Flat Appl) v t) (THead (Flat Appl) v t3)
                   by (sty1_sing . . . . H1 . previous)
sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t3)
          we proved sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t2)
       we proved 
          ∀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))