proposition: Lemma sigma_inv A s1 s x y : sigma s1 A = x ++ [s] ++ y -> ~ s el x -> ~ s el y -> ~ s el sym A -> s1 = s.
proof: Proof. rewrite sigma_eq. intros. cbn in H. assert (s el tau1 A ++ s1 :: rev (tau2 (gamma A))) by (rewrite H; eauto). eapply in_app_iff in H3 as [ | [ | ? % tau2_gamma]]; try firstorder using tau1_sym, tau2_sym. 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