diff options
| -rw-r--r-- | theories/FSets/FSetFacts.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 4c1c51c497..ac0227f5c2 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -287,6 +287,16 @@ End BoolSpec. (** * [E.eq] and [Equal] are setoid equalities *) +Definition E_ST : Setoid_Theory elt E.eq. +Proof. +constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. +Qed. + +Definition Equal_ST : Setoid_Theory t Equal. +Proof. +constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. +Qed. + Add Relation elt E.eq reflexivity proved by E.eq_refl symmetry proved by E.eq_sym |