proposition: Lemma minZF_elem' { p : peirce } x y u v : minZFeq' ⊢ x ≡' u → y ≡' v → x ∈' y → u ∈' v.
proof: Proof. assert (minZFeq' ⊢ ax_eq_elem'). apply Ctx. firstorder. apply (AllE x) in H. cbn in H. apply (AllE y) in H. cbn in H. apply (AllE u) in H. cbn in H. apply (AllE v) in H. cbn in H. subsimpl_in H. apply H. 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)