proposition: Theorem PCPb_entailment_minZFeq' : reduction minsolvable PCPb entailment_minZFeq'.
proof: Proof. intros B. split; intros H. - apply (@PCP_ZFD intu), (@rm_const_prv intu nil), soundness in H. intros D M rho H'. apply H, H'. - apply PCP_ZFeq'; try apply intensional_model. intros V M rho HM. apply PCPb_to_minZFeq.min_correct; trivial. apply H. now apply PCPb_to_minZFeq.min_axioms'. 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)