proposition: Lemma FST_pair_el' T x y z : FSTeq <<= T -> T ⊢ (z ≡ x ∨ z ≡ y) <-> T ⊢ z ∈ {x; y}.
proof: Proof. intros HT. setoid_rewrite FST_adj; auto. split; intros H; apply (DE H); auto. - apply DI2. apply FST_adj; auto. - assert1 H'. apply DI2. apply FST_adj in H'; auto. apply (DE H'); auto. apply Exp. eapply IE; try eapply (FST_eset'); auto. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets.FST Undecidability.FOL.FST Undecidability.FOL.Reductions.PCPb_to_FST Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)