proposition: Lemma parse_nonterminal_step_eq (valid : nonterminals_listT) (offset : nat) (len : nat) (pf : len <= len0) (nt : nonterminal_carrierT) : parse_nt_T_to_bool (parse_nonterminal_step str parse_nonterminal valid offset pf nt) = parse_nt_T_to_bool (parse_nonterminal_step str parse_nonterminal' valid offset pf nt).
proof: Proof. t ltac:(apply parse_productions'_eq). Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericBoolCorrectnessBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common Fiat.Common.Wf1