proposition: Corollary undecidable_entailment_binZF : undecidable entailment_binZF.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists binsolvable. apply PCPb_entailment_binZF. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.FOL.ZF_undec Undecidability.FOL.Sets.binZF Undecidability.FOL.Sets.Models.ZF_model Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Semantics.Tarski.FullSoundness Undecidability.FOL.ZF Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_ZFeq PCPb_to_ZFD PCPb_to_binZF) Undecidability.PCP(PCP PCP_undec Util.PCP_facts Reductions.PCPb_iff_dPCPb)