proposition: Theorem conservativity_back_ZF { p : peirce } phi : minZFeq ⊢T phi -> ZFeq ⊢T embed phi.
proof: Proof. intros [A[B HAB]] % minZF_decomp. apply prv_embed in HAB. exists ([ax_sep (embed psi) | psi ∈ A] ++ [ax_rep (embed psi) | psi ∈ B] ++ ZFeq'). split. - intros psi [H|[H|H] % in_app_iff] % in_app_iff; try now constructor. + apply in_map_iff in H as [psi'[<- H]]. constructor 2. + apply in_map_iff in H as [psi'[<- H]]. constructor 3. - apply (prv_cut HAB). intros psi' [psi [<- [[H|H] % in_app_iff|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]. + apply in_map_iff in H as [theta [<- H]]. apply Ctx. apply in_app_iff. right. apply in_app_iff. left. apply in_map_iff. exists theta. split; trivial. cbn. unfold ax_rep, fun_rel. rewrite !embed_subst. setoid_rewrite subst_ext at 1. setoid_rewrite subst_ext at 2. setoid_rewrite subst_ext at 3. setoid_rewrite subst_ext at 4. reflexivity. all: 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)