proposition: Lemma list_to_productions_to_nonterminal nt : Lookup_string G (default_to_nonterminal nt) = Lookup_idx G nt.
proof: Proof. unfold Lookup_string, Lookup_idx. unfold list_to_productions at 1; simpl. unfold productions, production in *. rewrite <- find_first_index_error by exact bl. rewrite default_find_to_nonterminal. set (ls' := pregrammar_productions G); clearbody ls'. revert nt; induction ls' as [|x xs IHxs]; simpl; intro nt; destruct nt; simpl; trivial; rewrite <- IHxs; clear IHxs. edestruct @Compare_dec.leb; simpl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common.Enumerable Fiat.Common.Enumerable.BoolProp Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Equality Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Common.Gensym Fiat.Common.Tactics.BreakMatch Fiat.Common.Tactics.DestructHead