proposition: Lemma undecidable_FOLstar_prv_class : undecidable FOL*_prv_class.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists (fun R => F R). intros R. apply (BPCP_CND R). Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.PCP.PCP_undec Undecidability.FOL.FOL Undecidability.FOL.Reductions(PCPb_to_FOL PCPb_to_FOL_intu PCPb_to_FOL_class)