proposition: Theorem undecidable_deduction_minZF' : undecidable deduction_minZF'.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists minsolvable. apply PCPb_deduction_minZF'. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.FOL.ZF_undec Undecidability.FOL.Sets.minZF Undecidability.FOL.Sets.Models.ZF_model Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Semantics.Tarski.FullSoundness Undecidability.FOL.ZF Undecidability.FOL.Reductions(PCPb_to_ZFeq PCPb_to_minZFeq PCPb_to_ZF PCPb_to_ZFD PCPb_to_binZF PCPb_to_minZF) Undecidability.PCP(PCP PCP_undec Util.PCP_facts Reductions.PCPb_iff_dPCPb)