proposition: Lemma simple_parse_of_production_correct_correct (str : String) (pat : production Char) : inhabited (parse_of_production G str pat) <-> exists p, simple_parse_of_production_correct G str pat p.
proof: Proof. split. { intros [p]; apply simple_parse_of_production_correct_correct_1; assumption. } { intros [p H]; eapply simple_parse_of_production_correct_correct_2; eassumption. } Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.SimpleCorrectness