Library Coq.Classes.Morphisms_Relations


Morphism instances for relations.

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

Require Import Relation_Definitions.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.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.