proposition: Lemma WfFix_eq : forall x, WfFix x == F (fun (y:A) (p:R y x) => WfFix y).
proof: Proof. intro x; unfold WfFix,Fix. case (Rwf x); simpl; intros. apply Fext; intros. apply Acc_iter_distr. Qed.
imports: ALEA(Probas) ALEA(Utheory)