fact: Definition UpdateAttributes {heading} (tup : @Tuple heading) (attrs : list (@sigT (@BoundedString _ (HeadingNames heading)) (fun attr => Domain heading (ibound (indexb attr)) -> Domain heading (ibound (indexb attr))))) : @Tuple heading := fold_left (fun (tup' : @Tuple heading) attr => UpdateAttribute tup' (projT1 attr) (projT2 attr)) attrs tup.
imports: Coq.Lists.List Coq.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.ilist2 Fiat.Common.StringBound Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Representation.Notations