The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Nov 18, 2014, at 11:33 , Robbert Krebbers 
> <mailinglists AT robbertkrebbers.nl>
>  wrote:
> 
> You probably have forgotten to prove a Proper for Vcons.

Robbert,

Thanks! I also suspected that that might be the problem. How I should 
formulate
Propper instantiation in this case? My first naive attempt:

Instance Vcons_Proper:
    Proper (equiv ==> equiv) (Vcons).

did not work. Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva