proposition: Lemma gp_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⟩⦆} {w} : θ ⊨ m1 ≈ m2 [{ wm }] -> (forall a1 a2, θ ⊨ f1 a1 ≈ f2 a2 [{ proj1_sig wf ⟨a1, a2⟩ }]) -> wm |= wf ≤ w -> θ ⊨ bind m1 f1 ≈ bind m2 f2 [{ w }].
proof: Proof. move=> ? ? ; apply weaken_rule2 ; apply seq_rule=> //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)