proposition: Lemma binsert_enumerate_length : forall (bag: BagType) (item: TItem), RepInv bag -> List.length (benumerate (binsert bag item)) = S (List.length (benumerate bag)).
proof: Proof. intros; rewrite binsert_enumerate; simpl; trivial. Qed.
imports: Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms