The Coq mailing list

[brandon_m_moore AT yahoo.com]

The code seems to work correctly after replacing

Definition hdT (a:T) : T :=
match a with
| E => E
| C _ y =>y
end.

by

Definition hdT (a:T) : T :=
match a with
| E => E
| C x _ =>x
end.