> * The exported constructors compute to the real ones, also in > equalities. For instance, [ true ] ≡ [ false ] computes to box true ≡ > box false. Out of interest: what would happen if [_] were made abstract? Dominique