Library Stdlib.Classes.Morphisms_Relations


Morphism instances for relations.

Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - University Paris Sud

From Stdlib Require Import Relation_Definitions.
From Stdlib.Classes Require Import Morphisms.
From Stdlib.Program Require Import Program.

Generalizable Variables A l.

Morphisms for relations
The instantiation at relation allows rewriting applications of relations R x y to R' x y when R and R' are in relation_equivalence.