proposition: Lemma nil_app_nil {X} (A : list X) : A = [] ++ A ++ [].
proof: Proof. now autorewrite with list. Qed.
imports: Setoid Morphisms List Arith Lia Undecidability.CFG.CFP Undecidability.CFG.CFG Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions