proposition: Lemma lookup_state_invalid_pre_Fix_grammar (nt : default_nonterminal_carrierT) (Hinvalid : is_valid_nonterminal initial_nonterminals_data nt = false) : lookup_state (pre_Fix_grammar initial_nonterminals_data) nt = default_value.
proof: Proof. unfold lookup_state, PositiveMapExtensions.find_default. pose proof (find_pre_Fix_grammar nt). rewrite Hinvalid in H; destruct H. unfold state in *; simpl in *. edestruct PositiveMap.find. { intuition congruence. } { 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