The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Hmm, that would be a bit tricky - as far as I know, Proper isn't really defined for functions taking dependent types.  I was able to get around it with my definition by using the fact that my @vector_cons A n was a simply typed function for each A, n.  Maybe you could define your own version of Vcons with arguments reordered, then provide trivial rewriting lemmas to convert Vcons to myVcons, and then you could use some Proper result on myVcons to do setoid rewriting.

I will try to do that. Although if that succeeds it would add an extra rewriting step to my proof where I want to use

this kind of rewriting. I guess if I really want to I can automate this via custom rewriting tactic...

Using Proper constructor types is a syntactic trick for generating the relation of two vectors having their elements pointwise equivalent, as an inductive relation:

OK, I think I got this. Thanks!

Sincerely,
Vadim