proposition: Lemma PPSpec_ran_universal : forall (w'' : A -> PPSpecMonad B), bind w w'' ≤[PPSpecMonad] w' -> forall a, w'' a ≤[PPSpecMonad] PPSpec_ran a.
proof: Proof. cbv. move=> ? [? H] a ; intuition. apply H. exists a ; intuition. Qed.
imports: Coq(ssreflect) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures Monoid)