proposition: Lemma minZF_sep { p : peirce } A phi : minZFeq' <<= A -> A ⊢ ax_sep' (rm_const_fm phi) → rm_const_fm (ax_sep phi).
proof: Proof. intros HA. apply II. assert1 H. cbn in *. eapply all_equiv. 2: apply Ctx; now left. intros [x|[]]. cbn. apply ex_equiv. intros B [y|[]] HB. cbn. apply all_equiv. intros [z|[]]. cbn. apply iff_equiv; intros C HC. 2: apply and_equiv. 1,2: apply elem_iff; intros psi; auto. rewrite !rm_const_fm_subst. cbn; subsimpl; rewrite !subst_comp. erewrite subst_ext; try reflexivity. now intros [|n]. 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)