proposition: Lemma parse_nonterminal_reified_opt_interp_correct : rinterp_parse (parse_nonterminal_reified G nt _) = BooleanRecognizer.parse_nonterminal (data := data) str nt.
proof: Proof. rewrite parse_nonterminal_reified_opt_interp_precorrect. apply parse_nonterminal_preopt_eq; assumption. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.BaseTypes Fiat.Parsers.BooleanRecognizerOptimized Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.ParserSyntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.ParserSemantics Fiat.Parsers.Reflective.SemanticsOptimized Fiat.Parsers.Reflective.ParserSemanticsOptimized Fiat.Parsers.Reflective.Morphisms Fiat.Parsers.Reflective.ParserReify Fiat.Parsers.Splitters.RDPList Fiat.Common