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