proposition: Lemma M_enc_stack_app A B : M_is_bunion (M_enc_stack A) (M_enc_stack B) (M_enc_stack (A ++ B)).
proof: Proof. Proof using M_FST VIEQ. induction A as [|[s t] A IH]; cbn. - repeat split; auto. intros x [] % M_eset. - repeat split. + intros x [->|H] % M_adj; apply M_adj; auto. right. now apply IH in H. + intros x H. apply M_adj. right. now apply IH in H. + intros x [->|H] % M_adj; rewrite M_adj; auto. apply IH in H. tauto. 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)