[Agda] Erasable vs. irrelevant

[jleivent at comcast.net]

I'm quite confused about these two concepts - as to whether they are the same or not.

Are all erasable terms irrelevant?  The confusing aspect to me is the requirement that irrelevant instances of the same type are treated as if they are all equal.  What if, instead of the instances being all equal, there just is no way to prove that two aren't equal?  Isn't that good enough to make them erasable (because no runtime decisions can be based on any differences in them)?  Are they then also irrelevant?  Or is this something that is erasable but not irrelevant?

-- Jonathan Leivent