proposition: Lemma find_aggregate_prestep st nt : PositiveMap.find nt (aggregate_prestep st) = option_map (step_constraints gdata (lookup_state st) (positive_to_nonterminal nt)) (PositiveMap.find nt st).
proof: Proof. unfold aggregate_prestep. autorewrite with aggregate_step_db. unfold from_aggregate_state, option_rect, option_map. 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