proposition: Lemma fold_grammar_correct str nt (p : parse_of G str (Lookup G nt)) : exists P, P str /\ related P (lookup_state fold_grammar (of_nonterminal nt)).
proof: Proof. destruct (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt)) eqn:Hvalid. { apply fold_grammar_correct_item; constructor. { apply initial_nonterminals_correct; assumption. } { assumption. } } { unfold fold_grammar. rewrite (lookup_state_invalid_pre_Fix_grammar _ G) by assumption. do 2 esplit; [ | eapply top_related ]. constructor. } Qed.
imports: Coq.Sets.Ensembles Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common