proposition: Lemma min_axioms_Z : (forall rho phi, Z phi -> rho ⊨ phi) -> forall rho phi, minZ phi -> rho ⊨ phi.
proof: Proof. Proof using M_ZF VIEQ. intros H rho phi []. - now apply min_axioms'. - cbn. specialize (H rho (ax_sep (embed phi0))). cbn in H. setoid_rewrite (subst_ext _ _ (($0 .: (fun m : nat => S (S (S m))) >> var) >> embed_t)) in H; try now intros []. rewrite <- embed_subst in H. setoid_rewrite min_embed in H. apply H. auto using Z. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets(minZF ZF) Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation)