DEFINITION tys3_gen_nil()
TYPE =
       ∀g:G.∀c:C.∀u:T.(tys3 g c TNil u)→(ex T λu0:T.ty3 g c u u0)
BODY =
Show proof