proposition: Lemma eq_opt_Lookup_idx 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 map_nth. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.OptionFacts