proposition: Lemma CountingList_BagUpdateCorrect : BagUpdateCorrect CountingList_RepInv CountingList_ValidUpdate CountingListAsBag_bfind apply ccontents bupdate_transform CountingListAsBag_bupdate.
proof: Proof. unfold BagUpdateCorrect, CountingList_RepInv. destruct container as [n l]. revert n; induction l; simpl; intros; split. - constructor. - constructor. - unfold CountingListAsBag_bupdate in *; simpl in *. destruct (IHl _ search_term update_term (refl_equal _) ). apply valid_update. unfold apply in *. destruct (search_term a); destruct (CountingListPartition l (search_term)); destruct (List.partition (search_term) l); simpl; auto. rewrite Permutation_app_comm; simpl. apply Permutation_cons_app; rewrite Permutation_app_comm; auto. - simpl in *; destruct (IHl _ search_term update_term (refl_equal _)). apply valid_update. unfold CountingListAsBag_bupdate in *; simpl in *. unfold apply 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