proposition: Lemma rdp_list_nonterminal_to_production_valid : forall nt, rdp_list_is_valid_nonterminal rdp_list_initial_nonterminals_data nt -> List.Forall rdp_list_production_carrier_valid (rdp_list_nonterminal_to_production nt).
proof: Proof. unfold rdp_list_production_carrier_valid, rdp_list_is_valid_nonterminal, rdp_list_initial_nonterminals_data, rdp_list_nonterminal_to_production. intros nt Hnt. apply Forall_map, Forall_forall; unfold compose; simpl; intros ? H. fix_list_bin_eq. apply list_in_bl in Hnt; [ | exact (fun n m => proj1 (Nat.eqb_eq n m)) ]. apply in_up_to_iff in Hnt. unfold default_production_carrier_valid; simpl. repeat (apply Bool.andb_true_iff; split); apply leb_iff. { rewrite map_length in Hnt. exact Hnt. } { apply in_up_to_iff in H. rewrite <- list_to_productions_to_nonterminal. exact H. } { omega. } 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