proposition: Lemma dec_lacc M : ldec M -> lacc M.
proof: Proof. intros [u [[cls_u lam_u] dec_u_M]]. exists (lam (u #0 I (lam Omega) I)); split. Lproc. + intros t. specialize (dec_u_M t). split; intros H; destruct dec_u_M; try tauto. * destruct H0 as [u_true ?]. eexists;split;[|eexists;reflexivity]. redSteps. rewrite u_true. destruct x. now Lsimpl. tauto. * destruct H0. destruct x. tauto. assert ((lam ((((u #0) I) (lam Omega)) I)) (enc t) == Omega). clear H. LsimplRed. rewrite H0. Lrewrite. now Lsimpl. destruct H as [H [? []]]. subst H. rewrite H2 in H3. destruct (Omega_diverges H3). Qed.