[Agda] Inconsistent rewrite behavior

[Martin Stone Davis]

I've noticed inconsistent behavior in the rewrite mechanism. An exemplar is
shown here <http://lpaste.net/143252>, where I've been making revisions to
Data.AVL. See my comments in the last function, lemjl-. When I rewrite v₂ ≡
v₁ and check the context of a goal, I find that one of the variables of
interest has been rewritten but another has not. Is this expected behavior?

P.s. This uses Agda 2.4.2.4 and a pull of the std-lib at 2.4.2.3.
--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151018/63d2f9c4/attachment.html