proposition: Lemma parse_productions'_ext (offset : nat) (len0_minus_len : nat) (prods : list production_carrierT) : parse_productions' (len0 := len0) str parse_nonterminal offset len0_minus_len prods = parse_productions' (len0 := len0) str parse_nonterminal' offset len0_minus_len prods.
proof: Proof. t_ext ltac:(erewrite parse_production'_for_ext || expand'). Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Common Fiat.Common.Equality Fiat.Common.List.ListMorphisms