Require Export reorder.
Section ListSubset.
Variable A : Type.
Lemma incl_empty : ∀(l : list A), incl [] l.
Lemma incl_left_tail : ∀(l1 l2 : list A)(a : A),
incl (a :: l1) l2 → incl l1 l2.
Lemma incl_lappl : ∀(l1 l2 l3 : list A),
incl (l1 ++ l2) l3 → incl l1 l3.
Lemma incl_lappr : ∀(l1 l2 l3 : list A),
incl (l1 ++ l2) l3 → incl l2 l3.
Lemma incl_list_reorder : ∀(l1 l2 : list A),
list_reorder l1 l2 → incl l1 l2.
Lemma list_reorder_incl_both : ∀(l1 l2 l3 l4 : list A),
list_reorder l1 l2 →
list_reorder l3 l4 →
incl l2 l3 →
incl l1 l4.
Lemma incl_rev : ∀(l : list A), incl (rev l) l.
Lemma incl_flatten_every :
∀(ll : list (list A))(l : list A),
every_nth (fun(lx : list A) ⇒ incl lx l) ll →
incl (flatten ll) l.
Definition lists_disjoint(l1 l2 : list A) : Prop :=
∀(a : A), (In a l1 → ¬ In a l2) ∧ (In a l2 → ¬ In a l1).
Lemma lists_disjoint_right_empty : ∀(l : list A),
lists_disjoint l [].
Lemma lists_disjoint_symm : ∀(l1 l2 : list A),
lists_disjoint l1 l2 → lists_disjoint l2 l1.
Lemma lists_disjoint_subset_right :
∀(l1 l2 l3 : list A),
incl l3 l2 →
lists_disjoint l1 l2 →
lists_disjoint l1 l3.
Lemma lists_disjoint_right_cons : ∀(l1 l2 : list A)(a : A),
lists_disjoint l1 l2 →
¬ In a l1 →
lists_disjoint l1 (a :: l2).
End ListSubset.
Implicit Arguments lists_disjoint [A].