src/Util/Unit.v


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.