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