[Agda] rewrite vs. with

[Jean-Philippe Bernardy]

I am referring to the substitutivity property of the equality you are using.

-- JP

On Wed, Sep 29, 2010 at 10:11 AM, David Leduc
<david.leduc6 at googlemail.com> wrote:
> Jean-Philippe Bernardy <bernardy at chalmers.se> wrote:
>> * use 'subst' on the equality of choice at the moment you need it.
>> Unfortunately that is a bit tedious.
>
> What is 'subst'???
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>