proposition: Lemma pre_Fix_grammar_helper_fixed st (H : aggregate_state_eq st (aggregate_step st)) : aggregate_state_eq st (pre_Fix_grammar_helper st).
proof: Proof. unfold pre_Fix_grammar_helper. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). edestruct dec; [ | 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