proposition: Lemma pointwise_pointwise (R : relation B) : relation_equivalence (pointwise_relation A R) (@eq A ==> R).
proof: Proof. intros. split; reduce; subst; firstorder. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses