proposition: Lemma seq_rule {A1 A2 B1 B2} {m1 : M1 A1} {m2 : M2 A2} {wm} {f1 : A1 -> M1 B1} {f2 : A2 -> M2 B2} {wf : OrdCat⦅Jprod ⟨A1,A2⟩ ; W ⟨B1, B2⟩⦆} : ⊨ m1 ≈ m2 [{ wm }] -> (forall a1 a2, ⊨ f1 a1 ≈ f2 a2 [{ wf∙1 ⟨a1, a2⟩ }]) -> ⊨ bind m1 f1 ≈ bind m2 f2 [{ wm |= wf }].
proof: Proof. intros Hm Hf. rewrite /semantic_judgement; etransitivity. apply: (rlmm_law2 _ _ M12 W θ _ _ (to_prod f1 f2) ⟨m1, m2⟩). set f12 := ((θ _ ∙ _) ∙ _); etransitivity. 2: apply: (ord_relmon_bind_proper W _ _ f12); move=> [? ?] ; apply Hf. apply: ((ord_relmon_bind W f12)∙2 _ _); apply: Hm. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)