proposition: Lemma FST_adj T x y z : FSTeq <<= T -> T ⊢ x ∈ y ::: z <-> T ⊢ x ≡ y ∨ x ∈ z.
proof: Proof. intros HT. assert (HA : T ⊢ ax_adj) by (apply Ctx; firstorder). apply (AllE z), (AllE y), (AllE x) in HA; cbn in HA. subsimpl_in HA. split; intros H; eapply IE; try apply H. - now apply CE1 in HA. - now apply CE2 in HA. 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)