fact: Definition parse_nonterminal_step_ext (valid : nonterminals_listT) (offset : nat) (len : nat) (pf pf' : len <= len0) (nt : nonterminal_carrierT) : parse_nonterminal_step str parse_nonterminal valid offset pf nt = parse_nonterminal_step str parse_nonterminal' valid offset pf' nt.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Common Fiat.Common.Equality Fiat.Common.List.ListMorphisms