proposition: Lemma elem_iff { p : peirce } A x y : minZFeq' <<= A -> A ⊢ ∃ $0 ≡' $(S x) ∧ (∃ $0 ≡' $(S (S y)) ∧ $1 ∈' $0) <-> A ⊢ $x ∈' $y.
proof: Proof. intros HA. split; intros H. - use_exists' H x'. clear H. assert1 H. apply CE in H as [_ H]. use_exists' H y'. eapply minZF_elem; auto. 1,2: eapply CE1; eauto. eapply CE2; auto. - apply ExI with $x. cbn. apply CI; try apply minZF_refl; auto. apply ExI with $y. cbn. apply CI; try apply minZF_refl; 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)