proposition: Lemma mu_spec : converges (mu P) <-> exists n : nat, P (ext n) == ext true.
proof: Proof. Proof using P_proc dec'_P. split. - intros (? & ? & ?). eapply mu_sound in H as (? & ? & ? & ?); eauto. - intros []. eapply mu_complete in H as []. exists (ext x0). split. eauto. eapply proc_ext. Qed.