fact: Definition item_rvalid (it : item Char) := match it with | Terminal _ => true | NonTerminal nt' => is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt') end.
imports: Coq.Strings.String Coq.Lists.List Coq.Arith.PeanoNat Fiat.Parsers.StringLike.Core Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Valid