proposition: Lemma pointwise_pointwise {B} (R : crelation B) : relation_equivalence (pointwise_relation R) (@eq A ==> R).
proof: Proof. intros. split. - simpl_crelation. - firstorder. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses