[Agda] Proving _!_ is inverse of tabulate...

[Jean-Philippe Bernardy]

On Fri, Apr 15, 2011 at 5:14 AM, Jason Dusek <jason.dusek at gmail.com> wrote:

>  So to do this out "longhand", I could have included something
>  in a `where', perhaps? There I would have explicitly matched
>  on [myLemma xs] and called the inner worker recursively?

You need to do a "with" simultaneously on the side of the equation
you wish rewritten, and on the proof. Then, match on the proof (refl).

Cheers,
JP.