proposition: Theorem conservativity_ZF' { p : peirce } phi : ZFeq' ⊢ embed phi -> minZFeq' ⊢ phi.
proof: Proof. intros H. apply (@rm_const_prv _ nil) in H. cbn in H. now apply loop_deductive'. Qed.
imports: Undecidability.FOL(Semantics.Tarski.FullFacts Syntax.Facts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF minZF) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_minZF PCPb_to_ZFD) Undecidability(Shared.ListAutomation)