blob: de137d39d13c007cabe1f2e1c257cde5cdb2e397 (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Setoid.
Parameter value' : Type.
Parameter equiv' : value' -> value' -> Prop.
Add Parametric Relation : _ equiv'
reflexivity proved by (Equivalence.equiv_reflexive _)
transitivity proved by (Equivalence.equiv_transitive _)
as apply_equiv'_rel.
|
