proposition: Lemma binsert_enumerate_weak : forall item inserted container, RepInv container -> (List.In item (benumerate (binsert container inserted)) <-> List.In item (benumerate container) \/ item = inserted).
proof: Proof. intros. rewrite <- refold_in. apply in_permutation_morphism; eauto using binsert_enumerate. Qed.
imports: Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms