blob: cf5c4f66993c3b59f4005a7395aa298b40b97954 (
plain)
1
2
3
4
5
6
7
8
|
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
(* an equivalence for a relation on trivial things, like [unit] *)
Global Instance Equivalence_trivial {A} : Equivalence (fun _ _ : A => True).
Proof.
repeat constructor.
Qed.
|