Lists as multisets

The subset relation on multi-sets is essential. I simply use list_reorder to define it.

Require Export reorder.

Section Multisets.

  Variable A : Type.

  Variable aeq : eq_type A.

  Definition multi_subset(l1 l2 : list A) : Prop :=
    (l3 : list A), list_reorder (l1 ++ l3) l2.

  Lemma multi_subset_trans : (l1 l2 l3 : list A),
    multi_subset l1 l2
    multi_subset l2 l3
      multi_subset l1 l3.

  Lemma multi_subset_antisymm : (l1 l2 : list A),
    multi_subset l1 l2
    multi_subset l2 l1
      list_reorder l1 l2.

End Multisets.

Implicit Arguments multi_subset [A].