proposition: Lemma fold_production_related (mapping : default_nonterminal_carrierT -> Ensemble String) st (Hmapping : forall nt, related (mapping nt) (st nt)) : forall pat, related (ensemble_fold_production' G mapping pat) (fold_production' st (opt.compile_production pat)).
proof: Proof. unfold ensemble_fold_production', fold_production' in *. induction pat as [|[|] xs IHxs]; simpl; eauto using on_nil_production_correct, combine_production_correct, on_terminal_correct. Qed.
imports: Coq.Sets.Ensembles Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Common.List.ListMorphisms