proposition: Lemma parse_nonterminal_or_abort_eq : forall (p : nat * nat) (valid : nonterminals_listT) (offset : nat) (len : nat) (pf : len <= fst p) (nt : nonterminal_carrierT), parse_nt_T_to_bool (parse_nonterminal_or_abort (gendata := gendata) str p valid offset pf nt) = parse_nt_T_to_bool (parse_nonterminal_or_abort (gendata := gendata') str p valid offset pf nt).
proof: Proof. t I. lazymatch goal with | [ |- ?f0 (Fix ?rwf ?P ?F ?x ?a ?b ?c ?d ?e) = ?f1 (Fix ?rwf ?Q ?G ?x ?a ?b ?c ?d ?e) ] => revert a b c d e; induction (rwf x); intros; rewrite !Wf1.Fix5_eq by (intros; apply parse_nonterminal_step_ext; trivial) end. apply parse_nonterminal_step_eq. auto with nocore. 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