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