proposition: Theorem Rice (M : term -> Prop) : (M <=1 proc) -> (forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) -> (exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) -> ~ ldec M.
proof: Proof. intros. intros A. assert (B : ldec M) by eassumption. destruct A as [u [proc_u Hu]]. destruct (Hu (lam Omega)) as [[] [eq m]]. - eapply Rice1; try eassumption. apply dec_lacc. exists u; tauto. - eapply Rice2; try eassumption. apply dec_lacc. apply ldec_complement. exists u; tauto. Qed.