Library ListSet

Fixpoint In {A:Set}(a:A) (l:list A) : Set :=
  match l with
  | nil ⇒ Empty_set
  | cons b m ⇒ (b = a) + In a m
  end.

Definition incl {A:Set} l m := ∀ a:A, In a l → In a m.
Hint Unfold incl : core.

Definition included {A:Set}(Gamma:list A)(T:A→Set) :=
  ∀ f, In f Gamma → T f.

Theorem in_eq {A:Set} : ∀ (a:A) l, In a (a :: l).

Theorem in_cons {A:Set} : ∀ (a b:A) l, In b l → In b (a :: l).

Lemma nil_included {A:Set} : ∀ (Ax:A→Set), included nil Ax.

Lemma nil_lem1 {A:Set} : ∀ l:list A, incl nil l.

Lemma in_app_or {A:Set} : ∀ l m (a:A), In a (l ++ m) → In a l + In a m.

Lemma in_or_app {A:Set} : ∀ l m (a:A), In a l + In a m → In a (l ++ m).

Lemma included_lem1 {A:Set} : ∀ l1 l2:list A, ∀ Ax:A→Set,
    included l1 Ax → included l2 Ax → included (l1++l2) Ax.

Lemma incl_tran {A:Set} : ∀ l m n:list A, incl l m → incl m n → incl l n.

Lemma incl_refl {A:Set} : ∀ l:list A, incl l l.
Hint Resolve incl_refl : core.

Theorem in_dec {A:Set} :
  (∀ x y:A, {x = y} + {x ≠ y}) →
  ∀ (a:A) (l:list A), In a l + (In a l → Empty_set).

Lemma incl_appl {A:Set} : ∀ l m n:list A, incl l n → incl l (n ++ m).
Hint Immediate incl_appl : core.

Lemma incl_appr {A:Set} : ∀ l m n:list A, incl l n → incl l (m ++ n).
Hint Immediate incl_appr : core.

Lemma in_inv {A:Set} : ∀ (a b:A) (l:list A), In b (a :: l) → (a = b) + In b l.