proposition: Lemma tau_eq_iff A a : ~ a el sym A -> tau1 A = tau2 A <-> palin (sigma a (gamma A)).
proof: Proof. rewrite sigma_gamma. unfold palin. rewrite !rev_app_distr, rev_involutive, <- app_assoc. intros Ha. split. - now intros ->. - intros H'. eapply list_prefix_inv in H'; intuition idtac; apply Ha. + now apply tau1_sym. + now apply tau2_sym. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions