proposition: Lemma WfFix_ind : (forall x f, (forall y (p:R y x), P (f y p)) -> P (F f)) -> forall x, P (WfFix x).
proof: Proof. intros; pattern x; apply well_founded_ind with (R:=R); trivial; intros. apply Pext with (m1:= F (fun (y:A) (p:R y x0) => WfFix y)). apply Oeq_sym; apply WfFix_eq. apply H; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)