proposition: Lemma pointwise_Reflexive {A B R} {_ : @Reflexive B R} : Reflexive (pointwise_relation A R).
proof: Proof. repeat intro; reflexivity. Qed.
imports: Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.RelationClasses Coq.Classes.Morphisms Fiat.Common.Coq__8_4__8_5__Compat