proposition: Lemma ProdBag_Empty_RepInv : ProdBag_RepInv ProdBag_bempty.
proof: Proof. unfold ProdBag_RepInv, ProdBag_bempty; intuition; simpl; [ apply bempty_RepInv | apply bempty_RepInv | ]. assert (forall A (ls ls' : list A), ls = nil -> ls' = nil -> Permutation ls ls') as perm_nil by (intuition; subst; constructor). assert (forall A (ls : list A), (forall a, ~ List.In a ls) -> ls = nil) as emp. intros; destruct ls; eauto; specialize (H a); simpl in H; tauto. eapply perm_nil. eapply emp; eapply benumerate_empty. eapply emp; eapply benumerate_empty. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties