proposition: Lemma weaken_rule2 {A B} {c1 : M1 A} {c2 : M2 B} {w w'} : ⊨ c1 ≈ c2 [{ w }] -> w ≤ w' -> ⊨ c1 ≈ c2 [{ w' }].
proof: Proof. rewrite /semantic_judgement. move=> ? ? ; etransitivity ; eassumption. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)