proposition: Lemma parse_nonterminal'_proj nt : parse_nonterminal' (proj str) nt = parse_nonterminal' str nt.
proof: Proof. unfold parse_nonterminal'. rewrite length_proj. apply parse_nonterminal_or_abort_proj. Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf1 Fiat.Common.SetoidInstances Fiat.Parsers.GenericRecognizer