proposition: Lemma sigma_eq s A : sigma s A = tau1 A ++ [s] ++ rev (tau2 (gamma A)).
proof: Proof. induction A as [ | [u v] ]. - reflexivity. - cbn. rewrite IHA. rewrite <- !app_assoc. now simpl_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