A different definition of types

Though alpha-equivalent types are not always considered to be equivalent, a notation that identifies alpha-equivalent types might be useful. Analogously to the redefinition of lambda-terms, we can redefine types.

A type is a binary tree, together with a partition of its leaves.