proposition: Lemma sigma_snoc A (x y u v: list sig) (s s': sig) : sigma s A = x ++ [s] ++ y -> ~ s el x -> ~ s el y -> sigma s' (A ++ [(u, v)]) = x ++ u ++ s' ++ v ++ y.
proof: Proof. rewrite !sigma_eq. unfold gamma. cbn. simpl_list. cbn. simpl_list. cbn. intros. eapply list_prefix_inv in H as [-> <-]; eauto. eapply notInZero. eapply (f_equal (fun a => count a s)) in H. rewrite <- !countSplit in H. cbn in H. rewrite !Nat.eqb_refl in H. eapply notInZero in H0. eapply notInZero in H1. rewrite H0, H1 in *. lia. 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