fact: Definition size_of_parse_item' (size_of_parse : forall {str pats} (p : parse_of G str pats), nat) {str it} (p : parse_of_item G str it) : nat := match p with | ParseTerminal _ _ _ _ => 0 | ParseNonTerminal _ _ p' => S (size_of_parse p') end.
imports: Coq.Strings.String Coq.Arith.Wf_nat Coq.Relations.Relation_Definitions Fiat.Parsers.ContextFreeGrammar.Core