General code for automatically proving type-bijection results in src/1.

This code was already used in the prototypical nominal datatype
package code; now it's more generally available. The code implements
one big function (for the moment) that proves all the nice results
(various rewrite rules) that are immediate consequences of the usual
type bijection theorem. In addition, the function defines the abs-rep
constants with stereotyped names.