proposition: Corollary seq_rule_ch_T { A1 A2 : ord_choiceType } { a1 : A1 } { a2 : A2 } { B1 B2 : ord_choiceType } {f1 : A1 -> MFreePr B1} {f2 : A2 -> MFreePr B2} (m1 : MFreePr A1) (m2 : MFreePr A2) (P : Prop) (Q : B1 -> B2 -> Prop) (judge1 : ⊨ ⦃ P ⦄ m1 ≈ m2 ⦃ fun _ _ => True ⦄ ) (judge2 : forall a1 a2, ⊨ ⦃ True ⦄ (f1 a1) ≈ (f2 a2) ⦃ Q ⦄ ) : ⊨ ⦃ P ⦄ x ∈ A1 <<- m1 ;; f1 x ≈ x ∈ A2 <<- m2 ;; f2 x ⦃ Q ⦄.
proof: Proof. by apply: (seq_rule_ch m1 m2 P (fun _ _ => True) Q judge1 judge2). 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)