fact: Definition size_of_parse_step {str pats} (p : parse_of G str pats) : nat := match p with | ParseHead _ _ p' => S (@size_of_parse_production _ _ p') | ParseTail _ _ p' => S (@size_of_parse _ _ p') end.
imports: Coq.Strings.String Coq.Arith.Wf_nat Coq.Relations.Relation_Definitions Fiat.Parsers.ContextFreeGrammar.Core