Library Coq.Classes.Morphisms_Relations



Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.Program.

Morphisms for relations
The instanciation at relation allows to rewrite applications of relations R x y to R' x y