proposition: Lemma Post_CFG_1' A : A <<= R -> A = [] \/ rewt G [S] (sigma a A).
proof: Proof. induction A. - cbn. eauto. - intros H. assert (A <<= R) by (eapply incl_cons_inv; eassumption). eapply IHA in H0. destruct a0 as [u v]. destruct H0. + subst. right. erewrite rewrite_sing with (x := u ++ [a] ++ v). { reflexivity. } right. eapply in_app_iff. right. eapply in_map_iff. exists (u,v); eauto. + right. erewrite rewrite_sing with (x := u ++ [S] ++ v). { now rewrite H0. } right. eapply in_app_iff. left. eapply in_map_iff. exists (u,v); eauto. 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