DEFINITION tys3_ind()
TYPE =
       ∀g:G
         .∀c:C
           .∀P:TList→T→Prop
             .∀t:T.∀t1:T.(ty3 g c t t1)→(P TNil t)
               →(∀t:T.∀t1:T.(ty3 g c t t1)→∀t2:TList.(tys3 g c t2 t1)→(P t2 t1)→(P (TCons t t2) t1)
                    →∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1))
BODY =
        assume g: G
        assume c: C
        assume P: TList→T→Prop
        suppose H: ∀t:T.∀t1:T.(ty3 g c t t1)→(P TNil t)
        suppose H1: ∀t:T.∀t1:T.(ty3 g c t t1)→∀t2:TList.(tys3 g c t2 t1)→(P t2 t1)→(P (TCons t t2) t1)
          (aux) by well-founded reasoning we prove ∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1)
           assume t: TList
           assume t1: T
           suppose H2: tys3 g c t t1
             by cases on H2 we prove P t t1
                case tys3_nil t2:T t3:T H3:ty3 g c t2 t3 ⇒
                   the thesis becomes P TNil t2
                   by (H . . H3)
P TNil t2
                case tys3_cons t2:T t3:T H3:ty3 g c t2 t3 t4:TList H4:tys3 g c t4 t3 ⇒
                   the thesis becomes P (TCons t2 t4) t3
                   by (aux . . H4)
                   we proved P t4 t3
                   by (H1 . . H3 . H4 previous)
P (TCons t2 t4) t3
             we proved P t t1
∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1)
          done
          consider aux
          we proved ∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1)
       we proved 
          ∀g:G
            .∀c:C
              .∀P:TList→T→Prop
                .∀t:T.∀t1:T.(ty3 g c t t1)→(P TNil t)
                  →(∀t:T.∀t1:T.(ty3 g c t t1)→∀t2:TList.(tys3 g c t2 t1)→(P t2 t1)→(P (TCons t t2) t1)
                       →∀t:TList.∀t1:T.(tys3 g c t t1)→(P t t1))