proposition: Lemma parse_nonterminal'_proj (nt : @nonterminal_carrierT Char predata) : parse_nonterminal' (proj str) nt = parse_nonterminal' str nt.
proof: Proof. refine (parse_nonterminal'_proj _ _); assumption. Qed.
imports: Fiat.Parsers.GenericRecognizerEquality Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BooleanRecognizer