proposition: Theorem conservativity_Z { p : peirce } phi : Zeq ⊢T embed phi -> minZeq ⊢T phi.
proof: Proof. intros [A HA] % Z_decomp. apply rm_const_prv in HA. rewrite map_map in HA. apply loop_deductive' in HA; auto. exists ([ax_sep' (rm_const_fm psi) | psi ∈ A] ++ minZFeq'). split. - intros psi [H|H] % in_app_iff; try now constructor. apply in_map_iff in H as [psi'[<- H]]. constructor 2. - apply (prv_cut HA). intros psi [[psi' [<- H]] % in_map_iff|H] % in_app_iff; auto. eapply IE; try apply minZF_sep; auto. apply Ctx, in_app_iff. left. refine (in_map _ _ _ H). 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)