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