proposition: Lemma terminal_iff_G y : terminal G y <-> ~ S el y.
proof: Proof. unfold terminal. enough ((exists y0, rew_cfg G y y0) <-> S el y). { firstorder. } split. - intros [y0 ?]. inversion H. subst. clear H. cbn in H0. destruct H0 as [ | [ [[] []] % in_map_iff | [[] []] % in_map_iff ] % in_app_iff]; inversion H; subst; eauto. - intros (u' & v' & ?) % List.in_split. subst. exists (u' ++ [S] ++ v'). econstructor. cbn. 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