proposition: Lemma tau2_app {X : Type} (A B: stack X) : tau2 (A ++ B) = tau2 A ++ tau2 B.
proof: Proof. induction A; cbn; auto. destruct a. rewrite <- app_assoc. congruence. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)