proposition: Lemma fold_grammar_correct_item str nt (p : parse_of_item G str (NonTerminal nt)) : exists P, P str /\ related P (lookup_state fold_grammar (opt.compile_nonterminal nt)).
proof: Proof. pose proof (@state_of_parse_item _ _ p) as p'. unfold fold_item' in p'. exists (er_ensemble p'). split; [ apply p' | ]. eapply (related_monotonic _); apply p'. 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