proposition: Lemma sigma_gamma a A : sigma a (gamma A) = tau1 A ++ a ++ rev (tau2 A).
proof: Proof. induction A as [ | (x & y) ]; unfold gamma in *; cbn. - reflexivity. - rewrite IHA. now rewrite rev_app_distr, <- !app_assoc. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions