proposition: Lemma Acc_iter_distr : forall x, forall r s : Acc R x, Acc_iter (fun _=> Distr B) F r == Acc_iter (fun _=> Distr B) F s.
proof: Proof. intros x r; elim r using Acc_inv_dep; simpl; intros. case s; simpl; intros. apply Fext; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)