fact: Record Morphism (X Y : RSetoid) := {evalMorphism :> X -> Y ;Morphism_prf : forall x1 x2, (st_eq x1 x2) -> (st_eq (evalMorphism x1) (evalMorphism x2)) }.
imports: Coq.Setoids.Setoid (hints) MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra