proposition: Lemma ensemble_fold_constraints_ext f g (H : forall x, f x = g x) nt : ensemble_fold_constraints f nt = ensemble_fold_constraints g nt.
proof: Proof. unfold ensemble_fold_constraints. apply ensemble_fold_productions'_ext. intro; apply H. 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