fact: Definition default_relation `{DefaultRelation A R} := R.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Classes.Equivalence Coq.Program.Basics