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