proposition: Theorem seq_rule_ch { A1 A2 : ord_choiceType } { B1 B2 : ord_choiceType } {f1 : A1 -> MFreePr B1} {f2 : A2 -> MFreePr B2} (m1 : MFreePr A1) (m2 : MFreePr A2) (P : Prop) (R : A1 -> A2 -> Prop) (Q : B1 -> B2 -> Prop) (judge1 : ⊨ ⦃ P ⦄ m1 ≈ m2 ⦃ R ⦄ ) (judge2 : forall a1 a2, ⊨ ⦃ R a1 a2 ⦄ (f1 a1) ≈ (f2 a2) ⦃ Q ⦄ ) : ⊨ ⦃ P ⦄ x ∈ A1 <<- m1 ;; f1 x ≈ x ∈ A2 <<- m2 ;; f2 x ⦃ Q ⦄.
proof: Proof. rewrite /fromPrePost in judge1, judge2. destruct A1 as [A1 chA1]. destruct A2 as [A2 chA2]. destruct B1 as [B1 chB1]. destruct B2 as [B2 chB2]. assert (forall a1 a2, ⊨ (f1 a1) ≈ (f2 a2) [{ fromPrePost (R a1 a2) Q }]) as judge2W. { move => a1 a2. exact (judge2 a1 a2). } move: (bind_rule m1 m2 (fromPrePost P R) judge1 (fun a => fromPrePost (R (fst a) (snd a)) Q) judge2W ). move => HH. rewrite /fromPrePost. move : HH. rewrite /= /MonoCont_bind /fromPrePost /=. rewrite /semantic_judgement. move => HH /=. move => β Hβ. simpl in *. destruct Hβ as [Hbeta1 Hbeta2]. specialize (HH β). simpl in HH. destruct HH. split. exact (Hbeta1). move => a1 a2 Ha1a2. split. assumption. move => b1 b2 Hb1b2. specialize (Hbeta2 b1 b2). apply: Hbeta2. exact Hb1b2. destruct H as [s1 s2]. exists x. split. assumption. exact s2. 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)