proposition: Lemma simple_parse_of_item_correct_correct (str : String) (it : item Char) : inhabited (parse_of_item G str it) <-> exists p, simple_parse_of_item_correct G str it p.
proof: Proof. split. { intros [p]; apply simple_parse_of_item_correct_correct_1; assumption. } { intros [p H]; eapply simple_parse_of_item_correct_correct_2; eassumption. } Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.SimpleCorrectness