proposition: Lemma fold_productions'_correct valid0 f (Hsub : sub_nonterminals_listT valid0 initial_nonterminals_data) (IHf : forall nt nt_idx, of_nonterminal nt = nt_idx -> Pnt valid0 nt (f nt nt_idx)) pats : Ppats valid0 pats (fold_productions' f (opt.compile_productions pats)).
proof: Proof. unfold fold_productions'. induction pats as [ | x xs IHxs ]; intros. { simpl; apply Ppats_nil. } { simpl; apply Ppats_cons; trivial; []. { apply fold_production'_correct; trivial. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.OptionFacts