proposition: Lemma terminal_iff G x : terminal G x <-> forall s y, s el x -> ~ (s, y) el rules G.
proof: Proof. split. - intros H s y A B. apply H. destruct (@in_split _ _ _ A) as (l1 & l2 & ->). exists (l1 ++ y ++ l2). change (s :: l2) with ([s] ++ l2). now econstructor. - intros H1 [y H2]. inversion H2. subst. eapply (H1 _ 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