proposition: Lemma lookup_state_aggregate_prestep st nt : lookup_state (aggregate_prestep st) nt = option_rect (fun _ => _) (fun _ => step_constraints gdata (lookup_state st) nt (lookup_state st nt)) default_value (PositiveMap.find (nonterminal_to_positive nt) st).
proof: Proof. unfold lookup_state. unfold PositiveMapExtensions.find_default. rewrite find_aggregate_prestep. unfold lookup_state. rewrite nonterminal_to_positive_to_nonterminal. unfold PositiveMapExtensions.find_default. unfold state in *; simpl in *. edestruct PositiveMap.find; 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