proposition: Theorem PCP_FSTD { p : peirce } B : PCPb B -> FSTeq ⊢ solvable' B.
proof: Proof. intros H. apply Weak with nil; auto. change nil with (map embed' nil). apply prv_embed. apply impl_prv. rewrite rev_involutive, app_nil_r. change minZFeq' with (map rm_const_fm nil ++ minZFeq'). apply rm_const_prv. cbn. now apply PCP_ZFD. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts ZF FST) Undecidability.FOL.Sets(Models.Aczel Models.ZF_model ZF minZF FST) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_ZFeq PCPb_to_minZF PCPb_to_minZFeq PCPb_to_ZFD) Lia Undecidability.PCP(PCP) Undecidability(Shared.ListAutomation)