proposition: Lemma eq_opt_Lookup_idx (Hcompiled_productions : List.map opt.compile_productions (List.map snd (pregrammar_productions G)) = compiled_productions) n : opt_Lookup_idx n = opt.compile_productions (Lookup_idx G n).
proof: Proof. unfold opt_Lookup_idx, Lookup_idx; subst compiled_productions. change nil with (opt.compile_productions nil) at 1. rewrite List.map_nth. reflexivity. Qed.
imports: Coq.Sets.Ensembles Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Common.List.ListMorphisms