proposition: Lemma undecidable_FOL_valid_intu : undecidable FOL_valid_intu.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). apply PCPb_to_FOL_intu.kvalid_red. 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)