proposition: Lemma funRewrite : f = g -> forall a , f a = g a.
proof: Proof. move=> H. rewrite H. move=> a. reflexivity. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)