proposition: Lemma fold_productions_related (mapping : default_nonterminal_carrierT -> Ensemble String) st (Hmapping : forall nt, related (mapping nt) (st nt)) : forall pats, related (ensemble_fold_productions' G mapping pats) (fold_productions' st (opt.compile_productions pats)).
proof: Proof. unfold ensemble_fold_productions', fold_productions' in *. induction pats as [|[|] xs IHxs]; simpl; repeat match goal with | _ => solve [ eauto using top_related, bottom_related, lub_correct, fold_production_related ] | [ |- related (ensemble_least_upper_bound _ _) _ ] => apply lub_correct | [ |- related (ensemble_fold_production' _ _ _) _ ] => apply fold_production_related end. 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