proposition: Lemma spec_applied_ord_relmon_law2 : forall (A B : I) (f : OrdCat ⦅ J A; M B ⦆) x, (dnib M f)∙1 ( (η M A)∙1 x ) = f∙1 x.
proof: Proof. move=> A B f x. unshelve epose (aux := (ord_relmon_law2 M) _ _ _). shelve. shelve. exact f. apply (f_equal sval) in aux. simpl in aux. unshelve eapply equal_f in aux. exact x. simpl in aux. assumption. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)