proposition: Lemma CountingList_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv CountingList_RepInv CountingListAsBag_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, CountingList_RepInv, CountingListAsBag_bdelete; destruct container as [n l]; revert n; induction l; intros; simpl in *; eauto. destruct (search_term a); simpl. destruct n; simpl in *; [ discriminate | injection containerCorrect]; intros. pose proof (IHl n search_term H). destruct (CountingListPartition l search_term); simpl in *; eauto. destruct n; simpl in *; [ discriminate | injection containerCorrect]; intros. pose proof (IHl n search_term H). destruct (CountingListPartition l search_term); simpl in *; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts