proposition: Lemma apply_left {A B1 B2} {m1 : M1 A} {c1 : M1 B1} {c2 : M2 B2} {w1 w2 w} : θ ⊨ m1 ≈ skip [{ w1 }] -> θ ⊨ c1 ≈ c2 [{ w2 }] -> w1 |= OrdCat_cst w2 ≤ w -> θ ⊨ m1 ;; c1 ≈ c2 [{ w }].
proof: Proof. move=> H1 H2 ; apply weaken_rule2. enough (c2 = skip ;; c2) as ->. apply seq_rule=> //. rewrite /bind monad_law1 //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)