blob: 637c3daebcb4b7c10bee0ad8ce97a9eea0836b6c (
plain)
1
2
3
4
5
6
7
8
|
Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.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.
|
