proposition: Lemma apply_left_tot {A1 A2} {c1 : M1 A1} {c2 : M2 A2} {w1 w2 w} : θ ⊨ c1 ≈ skip [{ w1 }] -> (forall a1, θ ⊨ ret a1 ≈ c2 [{ w2 a1 }]) -> w1 |= OrdCat_lift' (fun a _ => w2 a) ≤ w -> θ ⊨ c1 ≈ c2 [{ w }].
proof: Proof. move=> H1 H2 ; apply weaken_rule2. enough (c2 = skip ;; c2) as ->. enough (c1 = bind c1 ret) as ->. apply seq_rule=> // ? ?; now eapply weaken_rule2=> //=. rewrite /bind monad_law2 //. rewrite /bind monad_law1 //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)