proposition: Lemma rdp_list_to_of_nonterminal : forall nt, List.In nt (Valid_nonterminals G) -> rdp_list_to_nonterminal (rdp_list_of_nonterminal nt) = nt.
proof: Proof. unfold rdp_list_to_nonterminal, rdp_list_of_nonterminal, default_to_nonterminal, default_of_nonterminal. intro nt. rewrite first_index_default_first_index_error. destruct (first_index_error (string_beq nt) valid_nonterminals) eqn:H'; t. 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