proposition: Lemma min_axioms' (rho : nat -> V) : rho ⊫ binZF.
proof: Proof. Proof using M_ZF. intros A [<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]; cbn. - intros x y H1 H2. apply eq_equiv. now apply M_ext. - intros x y u v H1 % eq_equiv H2 % eq_equiv. now apply set_equiv_elem'. - exists ∅. apply (@M_ZF rho ax_eset). cbn. tauto. - intros x y. exists ({x; y}). setoid_rewrite eq_equiv. apply (@M_ZF rho ax_pair). cbn. tauto. - intros x. exists (⋃ x). apply (@M_ZF rho ax_union). cbn. tauto. - intros x. exists (PP x). apply (@M_ZF rho ax_power). cbn. tauto. - exists ω. split. split. + exists ∅. split. apply (@M_ZF rho ax_eset). cbn. tauto. apply (@M_ZF rho ax_om1). cbn. tauto. + intros x Hx. exists (σ x). split. 2: apply (@M_ZF rho ax_om1); cbn; tauto. intros y. rewrite !eq_equiv. now apply sigma_el. + intros x [H1 H2]. apply (@M_ZF rho ax_om2); cbn. tauto. split. * destruct H1 as (e & E1 & E2). change (set_elem ∅ x). enough (set_equiv ∅ e) as -> by assumption. apply M_ext; trivial. all: intros y Hy; exfalso; try now apply E1 in Hy. apply (@M_ZF rho ax_eset) in Hy; trivial. unfold ZFeq', ZF'. auto 8. * intros d (s & S1 & S2) % H2. change (set_elem (σ d) x). enough (set_equiv (σ d) s) as -> by assumption. apply M_ext; trivial. all: intros y; rewrite sigma_el; trivial. all: setoid_rewrite eq_equiv in S1; apply S1. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Asimpl Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets(binZF ZF) Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation) Morphisms Undecidability.FOL(Reductions.PCPb_to_ZFeq)