proposition: Lemma fold_constraints_extR f g (H : forall x, R (f x) (g x)) nt : R (fold_constraints f nt) (fold_constraints g nt).
proof: Proof. unfold fold_constraints. apply fold_productions'_extR. intro; apply H. Defined.
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