proposition: Lemma mu_sound v : lambda v -> mu P == v -> exists n, v = ext n /\ P (ext n) == ext true /\ (forall n', n' < n -> P (ext n') == ext false).
proof: Proof. Proof using P_proc dec'_P. unfold mu. intros lv R. standardizeHypo 100. apply mu'_sound in R. - destruct R as [n ?]. exists n. intuition. apply unique_normal_forms;try Lproc. assumption. - split;[|Lproc]. apply equiv_lambda in R;auto. apply closed_star in R;Lproc. - intros. lia. Qed.