proposition: Lemma Mlet_eq_compat : forall (A B : Type) (m1 m2:Distr A) (M1 M2 : A-o> Distr B), m1 == m2 -> M1==M2 -> Mlet m1 M1 == Mlet m2 M2.
proof: Proof. intros; apply Ole_antisym; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)