fact: Definition IBagEnumerateEmpty (ibempty : TBag) (ibenumerate : TBag -> list TIndex) := forall idx, ~ List.In idx (ibenumerate ibempty).
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties