proposition: Lemma ZF_sub_union T x y : ZFeq' <<= T -> T ⊢ x ≡ y -> T ⊢ sub (⋃ x) (⋃ y).
proof: Proof. intros HT H. prv_all z. apply II. assert1 H'. assert (HU : (z ∈ ⋃ x :: T) ⊢ ax_union) by (apply Ctx; firstorder). apply (AllE x), (AllE z) in HU; cbn in HU; subsimpl_in HU. apply CE1 in HU. eapply (IE HU) in H'. use_exists H' u. clear H' HU. eapply ZF_union_el'; auto. apply CI. - eapply ZF_eq_elem. auto. apply ZF_refl'; auto. apply (Weak H); auto. eapply CE1; auto. - eapply CE2; auto. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)