proposition: Lemma related_aggregate_state_max initial_nonterminals_data (HRbot : R ⊥ ⊥) : aggregate_state_relation (aggregate_state_max gdata0 initial_nonterminals_data) (aggregate_state_max gdata1 initial_nonterminals_data).
proof: Proof. unfold aggregate_state_relation. rewrite PositiveMapExtensions.lift_relation_hetero_iff; intro k. rewrite !find_aggregate_state_max_exact. break_match; trivial. 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.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Common.FMapExtensions.Wf Fiat.Common Fiat.Common.OptionFacts Fiat.Common.SetoidInstances