proposition: Lemma rewrite_sing R a x : (a, x) el rules R -> rew_cfg R [a] x.
proof: Proof. intro. rewrite nil_app_nil, (nil_app_nil [a]). now econstructor. 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