Constants for under/over, to rewrite under binders using "context lemmas"
Note: this file does not require
ssreflect; it is both required by
ssrsetoid and *exported* by
ssrunder.
This preserves the following feature: we can use
Setoid without
requiring
ssreflect and use
ssreflect without requiring
Setoid.