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.