proposition: Theorem conservativity_back_Z { p : peirce } phi : minZeq ⊢T phi -> Zeq ⊢T embed phi.
proof: Proof. intros [A HA] % minZ_decomp. apply prv_embed in HA. exists ([ax_sep (embed psi) | psi ∈ A] ++ ZFeq'). 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|H] % in_app_iff]] % in_map_iff. + apply in_map_iff in H as [theta [<- H]]. apply Ctx. apply in_app_iff. left. apply in_map_iff. exists theta. split; trivial. cbn. unfold ax_sep. rewrite embed_subst. erewrite subst_ext; try reflexivity. now intros [|n]. + eapply Weak; try apply embed_ZF'; auto. 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)