[Agda] Termination checking with Lexicographic recursive calls

[Sergey Goncharov]

> because the with-abstraction can occur also after the equality 
> sign.

sorry, that is nonsense. "with" can only be before the equality sign.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5384 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200218/2b330c24/attachment.p7s>