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 =
Show proof