Unbound now supports "set" binders and GADTs

I have just uploaded version 0.3 of the Unbound library (and version 0.5 of RepLib). This version adds support for two major new features:

• The new permbind and setbind functions create binders that are alpha-equivalent “up to permutation”. For example, when quantifying over a list of type variables, their order really does not matter: \(\forall a b. a \to b \approx \forall b a. a \to b\). Unbound now lets you express this and takes it into account when testing alpha-equivalence.
• RepLib (and hence Unbound) now supports GADTs, as long as they do not contain any existential quantification.

Enjoy!