The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Dec 10, 2014, at 14:49 , Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
> 
> I just want to show the rewriting which I want to use in the different 
> context.

To give you some context: in my actual case I am trying to rewrite function 
parameter of 'Vector.map'. It involves dependent types and equality relation 
on vectors which I worked out but I did not want to show here as it is not 
relevant to the problem. The function I am replacing is also not as trivial 
as shown.

Sincerely,
Vadim Zaliva

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