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