proposition: Lemma rewrite_relation_eq_dom {A B R} `{RewriteRelation B R}: RewriteRelation (respectful (@Logic.eq A) R).
proof: Proof. split. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses