proposition: Lemma benumerate_empty_eq_nil : benumerate bempty = nil.
proof: Proof. pose proof (benumerate_empty) as not_in; unfold BagEnumerateEmpty in not_in. destruct (benumerate bempty) as [ | item ? ]; simpl in *; [ | exfalso; apply (not_in item) ]; eauto. Qed.
imports: Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms