DEFINITION sty1_ind()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀P:T→Prop
               .∀t:T.(sty0 g c t1 t)→(P t)
                 →(∀t:T.(sty1 g c t1 t)→(P t)→∀t2:T.(sty0 g c t t2)→(P t2)
                      →∀t:T.(sty1 g c t1 t)→(P t))
BODY =
        assume g: G
        assume c: C
        assume t1: T
        assume P: T→Prop
        suppose H: ∀t:T.(sty0 g c t1 t)→(P t)
        suppose H1: ∀t:T.(sty1 g c t1 t)→(P t)→∀t2:T.(sty0 g c t t2)→(P t2)
          (aux) by well-founded reasoning we prove ∀t:T.(sty1 g c t1 t)→(P t)
           assume t: T
           suppose H2: sty1 g c t1 t
             by cases on H2 we prove P t
                case sty1_sty0 t2:T H3:sty0 g c t1 t2 ⇒
                   the thesis becomes P t2
                   by (H . H3)
P t2
                case sty1_sing t2:T H3:sty1 g c t1 t2 t3:T H4:sty0 g c t2 t3 ⇒
                   the thesis becomes P t3
                   by (aux . H3)
                   we proved P t2
                   by (H1 . H3 previous . H4)
P t3
             we proved P t
∀t:T.(sty1 g c t1 t)→(P t)
          done
          consider aux
          we proved ∀t:T.(sty1 g c t1 t)→(P t)
       we proved 
          ∀g:G
            .∀c:C
              .∀t1:T
                .∀P:T→Prop
                  .∀t:T.(sty0 g c t1 t)→(P t)
                    →(∀t:T.(sty1 g c t1 t)→(P t)→∀t2:T.(sty0 g c t t2)→(P t2)
                         →∀t:T.(sty1 g c t1 t)→(P t))