proposition: Lemma sym_app P R : sym (P ++ R) = sym P ++ sym R.
proof: Proof. induction P as [ | [] ]; eauto; cbn; rewrite IHP. now rewrite <- ? app_assoc. 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)