proposition: Lemma rdp_list_is_valid_nonterminal_nth_error nt_idx : rdp_list_is_valid_nonterminal rdp_list_initial_nonterminals_data nt_idx <-> nth_error (pregrammar_productions G) nt_idx <> None.
proof: Proof. unfold rdp_list_is_valid_nonterminal; fix_eqs. transitivity (List.In nt_idx rdp_list_initial_nonterminals_data). { split; intro H. { apply list_in_bl in H; [ assumption | apply Nat.eqb_eq ]. } { apply list_in_lb; [ apply Nat.eqb_eq | assumption ]. } } unfold rdp_list_initial_nonterminals_data. rewrite <- in_up_to_iff, map_length. rewrite nth_error_Some; reflexivity. 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