proposition: Lemma nonterminal_to_production_correct' : forall nt, is_valid_nonterminal initial_nonterminals_data nt -> List.map to_production (nonterminal_to_production nt) = Lookup G (to_nonterminal nt).
proof: Proof. intros nt H. rewrite <- (of_to_nonterminal nt) at 1 by assumption. rewrite nonterminal_to_production_correct by (apply initial_nonterminals_correct'; assumption). reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes