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].