fact: Definition parse_of_item_wf {str it} : well_founded (@parse_of_item_lt str it) := well_founded_ltof _ _.
imports: Coq.Strings.String Coq.Arith.Wf_nat Coq.Relations.Relation_Definitions Fiat.Parsers.ContextFreeGrammar.Core