proposition: Lemma tau2_sym A : tau2 A <<= sym A.
proof: Proof. induction A as [ | (x & y) ]. - firstorder. - cbn. intros ? [ | ] % in_app_iff. rewrite ? in_app_iff. eauto. rewrite !in_app_iff. eauto. 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)