[Agda] rewrite vs. with

[Jean-Philippe Bernardy]

On Wed, Sep 29, 2010 at 9:06 AM, David Leduc
<david.leduc6 at googlemail.com> wrote:
> Thank you Jean-Philippe!
>
> It works in this example because "proj1 t" appears explicitly in my
> goal at the biginning and thus I can rewrite it. However in my
> development (too big to be posted here), the term to be rewritten only
> appear in the goal after I have filled it partly (i.e., I have
> replaced the initial hole by a term with holes). That's when I'd like
> to rewrite.

Your options are:

* extract the current goal as a lemma (can I have an emacs command for
that?) and use rewrite there or;
* use 'subst' on the equality of choice at the moment you need it.
Unfortunately that is a bit tedious.

Cheers,
JP.