proposition: Lemma bZF_adj { p : peirce } : binZF ⊢ ax_adj'.
proof: Proof. prv_all' x. prv_all' y. assert (H : binZF ⊢ ax_pair'). { apply Ctx. unfold binZF. auto. } apply (AllE y) in H. cbn in H. apply (AllE y) in H. cbn in H. use_exists' H sy. clear H. assert (H : binZF ⊢ ax_pair'). { apply Ctx. unfold binZF. auto. } apply (AllE x) in H. cbn in H. apply (AllE sy) in H. cbn in H. eapply Weak in H. use_exists' H pxy. clear H. 2: auto. assert (H : binZF ⊢ ax_union'). { apply Ctx. unfold binZF. auto. } apply (AllE pxy) in H. cbn in H. eapply Weak in H. use_exists' H a. clear H. 2: auto. apply (ExI a). cbn. subsimpl. prv_all' b. apply CI; apply II. - assert2 H. apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE1 in H. rewrite imps in H. eapply Weak in H. use_exists' H c. clear H. 2: auto. assert4 H. apply (AllE c) in H. cbn in H. subsimpl_in H. cbn in H. apply CE1 in H. eapply DE. eapply IE. apply H. eapply CE1. auto. + apply DI1. eapply bZF_elem. auto 7. * apply bZF_refl. auto 7. * apply Ctx. left. unfold eq'. cbn. unfold binZF.eq'. cbn. subsimpl. reflexivity. * eapply CE2. auto. + apply DI2. clear H. assert6 H. apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE1 in H. eapply DE. eapply IE; try apply H. * eapply bZF_elem. auto 7. 1: apply bZF_refl. auto 7. 2: eapply CE2; auto. apply Ctx. left. unfold eq'. cbn. subsimpl. reflexivity. * apply Ctx. left. unfold eq'. cbn. subsimpl. reflexivity. * apply Ctx. left. unfold eq'. cbn. subsimpl. reflexivity. - assert2 H. apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). eapply DE; try now apply Ctx. + apply (ExI x). cbn. subsimpl. apply CI; auto. clear H. assert4 H. apply (AllE x) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). apply DI1. unfold eq'. cbn. subsimpl. apply bZF_refl. auto 7. + apply (ExI sy). cbn. subsimpl. apply CI. * clear H. assert4 H. apply (AllE sy) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). apply DI2. unfold eq'. cbn. subsimpl. apply bZF_refl. auto 7. * clear H. assert5 H. apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). apply DI2. unfold eq'. cbn. subsimpl. auto. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Semantics.Tarski.FullSoundness Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Reductions.PCPb_to_binZF Undecidability.FOL.ZF Undecidability.FOL.FST Undecidability.FOL.Sets(Models.FST_model Models.ZF_model binFST binZF) Lia Undecidability(Shared.ListAutomation)