proposition: Theorem weaken_rule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {d1 : SDistr (Choice.Pack chA1)} {d2 : SDistr (Choice.Pack chA2)} : forall w w', (⊨ d1 ≈ d2 [{ w }]) -> w ≤ w' -> (⊨ d1 ≈ d2 [{ w' }] ).
proof: Proof. move => w w' Hjudg Hleq. rewrite /semantic_judgement /θ_morph //= /θ0 //=. unfold "≤". simpl. rewrite /MonoCont_order //=. move => π H'. move: (Hleq π H'). by apply: Hjudg. Qed.
imports: mathcomp(all_ssreflect all_algebra boolp distr reals realsum) Mon(SpecificationMonads SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd SubDistr Couplings Axioms)