proposition: Lemma myBetaRed : forall x e, (exist P x e)∙1 = x.
proof: Proof. move=> x e. simpl. reflexivity. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)