proposition: Lemma binFOL_prv_intu_undec : undecidable binFOL_prv_intu.
proof: Proof. apply (undecidability_from_reducibility undecidable_deduction_binZF), binZF_binFOL_prv_intu. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.PCP.PCP_undec Undecidability.FOL(binZF_undec FOL) Undecidability.FOL.Sets(binZF) Undecidability.FOL.ZF Undecidability.FOL.Syntax.Core Undecidability.FOL.Syntax.BinSig Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts