fact: Definition SuccessfulInsertSpec {qs_schema} (qs : QueryStructure qs_schema) (Ridx : _) (qs' : QueryStructure qs_schema) (tup : @IndexedRawTuple (GetNRelSchemaHeading (qschemaSchemas qs_schema) Ridx)) (result : bool) : Prop := decides result (forall t, GetRelation qs' Ridx t <-> (EnsembleInsert tup (GetRelation qs Ridx) t)).
imports: Coq.Lists.List Coq.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common.StringBound Fiat.Common.Ensembles.IndexedEnsembles Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure