proposition: Lemma CountingList_BagDeleteCorrect : BagDeleteCorrect CountingList_RepInv CountingListAsBag_bfind apply ccontents CountingListAsBag_bdelete.
proof: Proof. unfold BagDeleteCorrect, CountingList_RepInv; destruct container as [n l]; revert n; induction l; simpl; intros; split. + constructor. + constructor. + simpl in *; destruct (IHl _ search_term (refl_equal _)). unfold CountingListAsBag_bdelete in *; simpl in *. unfold apply in *. destruct (search_term a); destruct (CountingListPartition l (search_term)); destruct (List.partition (search_term) l); simpl; auto. + simpl in *; destruct (IHl _ search_term (refl_equal _)). unfold CountingListAsBag_bdelete in *; unfold apply in *; simpl in *. destruct (search_term a); destruct (CountingListPartition l (search_term)); destruct (List.partition (search_term) l); simpl; auto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts