proposition: Lemma fold_grammar_correct_item' str it (p : parse_of_item G str it) : exists P, P str /\ related P (fold_item' (lookup_state fold_grammar) (opt.compile_item it)).
proof: Proof. destruct p as [ch P Ppf Hch|] eqn:Hp. { simpl. eexists; split; [ | apply on_terminal_correct ]. eexists; split; eassumption. } { apply fold_grammar_correct_item; assumption. } 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