proposition: Lemma reachable_production_valid (its : production Char) (Hreach : production_is_reachable G its) : production_valid its.
proof: Proof. destruct Hreach as [nt [prefix [Hreach Hreach']]]. specialize (Hvalid nt Hreach). unfold productions_valid in Hvalid. rewrite Forall_forall in Hvalid. eapply production_valid_app. apply Hvalid; eassumption. Qed.
imports: Coq.Strings.String Coq.Lists.List Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Common Fiat.Common.UIP Fiat.Common.List.ListFacts