proposition: Lemma ret_rule2 {A B} {a : A} {b : B} : ⊨ ret a ≈ ret b [{ (ord_relmon_unit W ⟨A , B⟩)∙1 ⟨a,b⟩ }].
proof: Proof. apply: (rlmm_law1 _ _ M12 W θ ⟨A , B⟩ ⟨a,b⟩). Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)