The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

I'm trying to define a type which has a uniqueness property.  I thought
I'd define the type to be mutually inductive with a proposition type
indicating the uniqueness:

Parameter A : Set.
Axiom dec_eq_A : forall x y:A, {x=y} + {x<>y}.

Inductive uniq_list : Set :=
  | u_nil : uniq_list
  | u_cons : forall (x:A) (l:uniq_list),
             notin x l -> uniq_list

 with notin : var -> uniq_list -> Prop :=
  | notin_nil  : forall (v:var), notin v u_nil
  | notin_cons : forall (x v:var) (l:uniq_list),
                   v <> x -> notin v l -> 
                   notin v (u_cons x l).

However, coq rejects the definition, complaining,

Error: The reference uniq_list was not found in the current environment.


My question is twofold:

1) Why does this happen?
2) Is there a better way to do what I want? Is it possible?
(I know I could just use ListSet, but I'm actually interested in a more
complex structure).