DEFINITION tys3_gen_cons()
TYPE =
       ∀g:G
         .∀c:C
           .∀ts:TList.∀t:T.∀u:T.(tys3 g c (TCons t ts) u)→(land (ty3 g c t u) (tys3 g c ts u))
BODY =
Show proof