The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Dec 10, 2014, at 23:18 , Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>
>  wrote:
> 
> Unfortunately, you have never explained what kind of equivalence you need 
> on your functions. Your example showed an equivalence based on 
> eta-convertibility, so I gave you a way to do it.

I am trying to prove an expression:

equiv (Vcons_reord (Vmap (λ x0 : A, x0 * x) z) 1)
      (Vcons_reord (Vmap (mult x)           z) 1)


I can separately prove:

equiv (λ x0 : A, x0 * x) (mult x)

and I wanted to rewrite using this in the Vmap expression above.

Please note that order or arguments in the lambda expression is reversed, so 
it requires application of multiplication commutativity lemma which I have.

I could not seems to be able to apply directly in original goal. This is 
another thing
I want to learn. How to deal with lambda expressions within goals.

Thanks!

Sincerely,
Vadim Zaliva

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