proposition: Lemma wretract_fplusok : forall A (f:nat -> MF A), (forall x, wretract (fun k => f k x)) -> forall k, fplusok (f k) (sigma_fun f k).
proof: Proof. red; intros; intro x. apply (H x k); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)