proposition: Lemma parse_nonterminal_or_abort_minus_eq : forall (p : nat * nat) (valid : nonterminals_listT) (offset : nat) (len0_minus_len : nat) (nt : nonterminal_carrierT), parse_nt_T_to_bool (parse_nonterminal_or_abort_minus (gendata := gendata) str p valid offset len0_minus_len nt) = parse_nt_T_to_bool (parse_nonterminal_or_abort_minus (gendata := gendata') str p valid offset len0_minus_len nt).
proof: Proof. intros; apply parse_nonterminal_or_abort_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