Dedup_before.v

Require Import List.
Import ListNotations.

Section dedup.
  Variable A : Type.
  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.

  Fixpoint dedup (xs : list A) : list A :=
    match xs with
    | [] => []
    | x :: xs => let tail := dedup xs in
                 if in_dec A_eq_dec x xs then
                   tail
                 else
                   x :: tail
    end.

  Lemma dedup_In : forall (x : A) xs,
      In x xs ->
      In x (dedup xs).
  Proof using.
    induction xs; intros; simpl in *.
    - intuition.
    - case in_dec; intuition; subst; simpl; auto.
  Qed.
End dedup.