proposition: Lemma Por_correct_2 (s t:term) : converges (Por (ext s) (ext t)) -> exists (b:bool), Por (ext s) (ext t) == ext b.
proof: Proof. intros [v [R lv]]. unfold Por in R. LsimplHypo. evar (s':term). assert (C:converges s'). eexists. split. exact R. Lproc. subst s'. apply app_converges in C as [_ [v' [C lv']]]. assert (C':=C). apply mu_sound in C as [n [eq [R' H]]];try Lproc. - exists (doesHaltIn s n). subst. unfold Por. Lsimpl. rewrite C'. now Lsimpl. - eexists. now Lsimpl. Qed.