INDUCTIVE DEFINITION tys3 () [ :G, :C ]
OF ARITY TList→T→Prop
BUILT FROM:
     tys3_nil: ∀u:T.∀u0:T.(ty3 g c u u0)→(tys3 g c TNil u)
   | tys3_cons: ∀t:T.∀u:T.(ty3 g c t u)→∀ts:TList.(tys3 g c ts u)→(tys3 g c (TCons t ts) u)