fact: Definition equivalence_rewrite_relation `(eqa : Equivalence A eqA) : RewriteRelation eqA := Build_RewriteRelation _.
imports: Coq.Classes.Init Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions