fact: Definition size_of_maybe_empty_item' (size_of_maybe_empty_productions : forall {pats}, maybe_empty_productions G valid pats -> nat) {it} (p : maybe_empty_item G valid it) : nat := match p with | MaybeEmptyNonTerminal _ _ p' => S (size_of_maybe_empty_productions p') end.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.Reachable.MaybeEmpty.Core Fiat.Parsers.BaseTypes