[Agda] Irrelevance and propositional equality

[Alan Jeffrey]

I'm currently working on some code where life is remarkably easier if I 
make use of a function which promotes irrelevant propositional 
equalities to relevant ones:

  ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
  ≡-relevant a≡b = trustMe

Of course, life would also be remarkably easier if I were to postulate 
false. Am I shooting myself in the foot here?

A.