proposition: Lemma parse_nonterminal_reified_unfold_extensional : ParserSyntaxEquivalence.has_parse_term_equiv nil (parse_nonterminal_reified G nt Semantics.interp_TypeCode) (parse_nonterminal_reified G nt (PartialUnfold.normalized_of Semantics.interp_TypeCode)).
proof: Proof. unfold parse_nonterminal_reified, Syntactify.syntactify_rproductions, Syntactify.syntactify_prod, Syntactify.syntactify_string, Syntactify.syntactify_ritem_ascii; constructor. repeat build_term_equiv_step. repeat build_term_equiv_step. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.BaseTypes Fiat.Parsers.BooleanRecognizerOptimizedReflective Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Parsers.Reflective.ParserSoundnessOptimized Fiat.Parsers.Reflective.ParserPartialUnfold Fiat.Parsers.Splitters.RDPList Fiat.Parsers.StringLike.Core