[Agda] vertical bars | in my goal

[David Leduc]

Hi,

What does it mean when I have vertical bars | in my goal? And what
should be the shape of the corresponding proof?

Thank you!

David