[Agda] Again, a question on records

[David Leduc]

I wrote:
> You see here that the right record is inferred from the types of xi and y1.

I meant:
You see here that the right records are inferred from the types of x1
and y1 (resp., x2 and y2).