proposition: Lemma rdp_list_find_to_nonterminal idx : List.first_index_error (string_beq (rdp_list_to_nonterminal idx)) valid_nonterminals = bool_rect (fun _ => option _) (Some idx) (None) (Compare_dec.leb (S idx) (List.length valid_nonterminals)).
proof: Proof. apply default_find_to_nonterminal. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts