proposition: Lemma tau2_gamma s A : s el rev (tau2 (gamma A)) <-> s el tau2 A.
proof: Proof. induction A as [ | [u v] ]; cbn. - reflexivity. - simpl_list. rewrite !in_app_iff, IHA. firstorder. 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