proposition: Lemma ensemble_fold_production'_ext {f g} (ext : forall b, f b = g b) b : ensemble_fold_production' f b = ensemble_fold_production' g b.
proof: Proof. unfold ensemble_fold_production'. induction b as [ | x ]; try reflexivity; simpl in *; []. rewrite IHb; destruct x; rewrite ?ext; reflexivity. 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