Compatibility layer for
under and
setoid_rewrite.
This file is intended to be required by
Require Import Setoid.
In particular, we can use the
under tactic with other relations
than
eq or
iff, e.g. a
RewriteRelation, by doing:
Require Import ssreflect. Require Setoid.
This file's instances have priority 12 > other stdlib instances.
(Note: this file could be skipped when porting
under to stdlib2.)