The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

I have an inductive types to describe types in a programming language I
want to formalize. It looks like this:

Inductive ty: Set :=
  | tvar : id -> ty
  | tpoly : id -> list ty -> ty.

"id" is for identifiers and is just a wrapper around "nat"s.

I want to define equality for this type, both on the "Prop" level
and as a boolean function.

I tried to prove this theorem:

Definition ty_eq_dec (t1 t2 : ty) : {t1 = t2} + {t1 <> t2}.

using "decide equality", but this seems to go nowhere.

I defined an induction principle for "ty" as described in Sec. 14.3
of the Coq book, but it is not clear to me how I can use it
to prove ty_eq_dec.

What is the best way to go about this?

Klaus