proposition: Lemma find_pre_Fix_grammar_to_lookup_state' nt : PositiveMap.find nt (pre_Fix_grammar initial_nonterminals_data) = if is_valid_nonterminal initial_nonterminals_data (positive_to_nonterminal nt) then Some (lookup_state (pre_Fix_grammar initial_nonterminals_data) (positive_to_nonterminal nt)) else None.
proof: Proof. rewrite <- find_pre_Fix_grammar_to_lookup_state, positive_to_nonterminal_to_positive. reflexivity. Qed.
imports: Coq.Init.Wf Coq.Numbers.BinNums Coq.Arith.Arith Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.Splitters.RDPList Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common.FMapExtensions.Wf Fiat.Common Fiat.Common.OptionFacts Fiat.Common.SetoidInstances