fact: Fixpoint simple_parse_of_correct str pats t := @simple_parse_of_correct_step simple_parse_of_correct simple_parse_of_production_correct str pats t with simple_parse_of_production_correct str pat t := @simple_parse_of_production_correct_step simple_parse_of_production_correct simple_parse_of_item_correct str pat t with simple_parse_of_item_correct str it t := @simple_parse_of_item_correct_step simple_parse_of_correct str it t.
imports: Coq.Lists.List Fiat.Parsers.ContextFreeGrammar.Core