proposition: Lemma parse_production'_for_ext splits splits' (Hsplits : forall idx offset len, splits idx str offset len = splits' idx str offset len) (offset : nat) (len0_minus_len : nat) prod_idx : parse_production'_for (len0 := len0) str parse_nonterminal splits offset len0_minus_len prod_idx = parse_production'_for (len0 := len0) str parse_nonterminal' splits' offset len0_minus_len prod_idx.
proof: Proof. remember (to_production prod_idx) as prod eqn:Heq. unfold parse_production'_for. revert prod_idx Heq offset len0_minus_len splits splits' Hsplits ext; induction prod; simpl; intros; rewrite <- Heq; simpl; t_ext idtac. erewrite parse_item'_ext. { apply f_equal. specialize (IHprod (production_tl prod_idx)). rewrite production_tl_correct in IHprod. generalize dependent (to_production prod_idx); intros; subst. specialize (IHprod eq_refl). apply IHprod; clear IHprod; simpl; auto with nocore. } { auto with nocore. } Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Common Fiat.Common.Equality Fiat.Common.List.ListMorphisms