proposition: Lemma List_BagInsertEnumerate : BagInsertEnumerate ListBag_RepInv id (ListAsBag_binsert).
proof: Proof. firstorder. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface