proposition: Theorem pre_hypothesis_rule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {d1 : MFreePr (Choice.Pack chA1)} {d2 : MFreePr (Choice.Pack chA2)} : forall (pre : Prop) post, (pre -> ⊨ ⦃ True ⦄ d1 ≈ d2 ⦃ post ⦄) -> (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post ⦄).
proof: Proof. move => pre post Hjug. rewrite /semantic_judgement /θdex //= /θ0 //=. unfold "≤". simpl. rewrite /MonoCont_order //=. move => π H'. intuition. rename H into p. rename H1 into H. rename H0 into q. rewrite /semantic_judgement /θdex //= /θ0 //= in H. specialize (H π). unfold "≤" in H. simpl in H. rewrite /MonoCont_order //= in H. rewrite /SProp_op_order /Basics.flip in H. intuition. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod)