proposition: Lemma muF_pterm : pterm == muFone pterm.
proof: Proof. simpl; apply ford_eq_intro; intro x; unfold pterm. rewrite <- (mufix_mu (fun (x:A) => fone B) muFone F_muF_eq_one x). apply Oeq_trans with (muFone (mufix muFone) x); auto. apply (ford_eq_elim (A:=A)). apply (mufix_eq (F:=muFone)); auto. apply (ford_eq_elim (A:=A)). red; apply muF_stable; auto. simpl; apply ford_eq_intro; intro; auto. apply (mufix_mu (fun (x:A) => fone B) muFone F_muF_eq_one n). Qed.
imports: ALEA(Probas) ALEA(Utheory)