Lists as multisets
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].