proposition: Lemma gp_ret_rule {A B a b w} : proj1_sig (ord_relmon_unit W ⟨A , B⟩) ⟨a,b⟩ ≤ w -> θ ⊨ ret a ≈ ret b [{ w }].
proof: Proof. apply weaken_rule2 ; apply ret_rule2. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)