proposition: Lemma fold_nt'_correct (valid0 : nonterminals_listT) (valid0_len : nat) (Hlen : nonterminals_length valid0 <= valid0_len) (Hsub : sub_nonterminals_listT valid0 initial_nonterminals_data) : forall nt, Pnt valid0 nt (fold_nt' (compiled_productions G) valid0_len valid0 nt).
proof: Proof. intro nt; apply fold_cnt'_correct; auto. 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