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