proposition: Lemma fold_item'_extR {f g} (ext : forall b, R (f b) (g b)) b : R (fold_item' f b) (fold_item' g b).
proof: Proof. unfold fold_item'. generalize (@of_nonterminal _ (@rdp_list_predata _ G)); simpl; intro. generalize on_terminal; intro. unfold state in *. simpl in *. clear -ext R_Reflexive. abstract (destruct b; try apply ext; reflexivity). 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