proposition: Lemma sigma_gamma2 A : sigma # (gamma2 A) = tau2 A ++ [#] ++ gamma A.
proof: Proof. induction A as [ | (x,y) ] ; cbn. - reflexivity. - unfold gamma2 in IHA. cbn in *. rewrite IHA. now simpl_list. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions