proposition: Lemma parse_production'_for_eq (splits : production_carrierT -> String -> nat -> nat -> list nat) (offset : nat) (len0_minus_len : nat) (prod_idx : production_carrierT) : parse_production_T_to_bool (parse_production'_for (len0 := len0) str parse_nonterminal splits offset len0_minus_len prod_idx) = parse_production_T_to_bool (parse_production'_for (len0 := len0) str parse_nonterminal' splits offset len0_minus_len prod_idx).
proof: Proof. t I. repeat match goal with | [ |- context[list_rect ?P ?N ?C] ] => not is_var C; let P' := fresh "P'" in let N' := fresh "N'" in let C' := fresh "C'" in set (P' := P); set (N' := N); set (C' := C) end. generalize (to_production prod_idx); intro ps. revert prod_idx offset len0_minus_len. induction ps as [|p ps IHps]. { simpl; t I. } { simpl; t ltac:(apply parse_item'_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