proposition: Theorem Rice_classical (M : term -> Prop) : (M <=1 closed) -> (forall (s t : term), closed t -> M s -> (forall u, pi s u <-> pi t u) -> M t) -> (exists p, closed p /\ ~ M p) -> (exists p, closed p /\ M p) -> ~ ldec M.
proof: Proof. intros. eapply Scott. - firstorder. - intros. eapply H0; try eassumption. intros. unfold pi. now rewrite H5. - destruct H2; eauto. - destruct H2; eauto. Qed.