proposition: Lemma enc_stack_el' x A : x ∈ M_enc_stack A -> exists s t, (s, t) el A /\ x = M_enc_card s t.
proof: Proof. Proof using M_FST VIEQ. induction A as [|[s t] A IH]; cbn. - now intros H % M_eset. - intros [->|H] % M_adj. + exists s, t. intuition. + destruct (IH H) as (u&v&H'&->). exists u, v. intuition. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.FST Undecidability.FOL.Sets.FST Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)