[Agda] Irrelevance and equalities?

[Brandon Moore]

Might it be nice to define Dec like

data AltDec (P : Set) : Set where
  yes : P → AltDec P
  no : .(P → ⊥) → AltDec P

Then it can be proven that

mutual
  lemm : {P : Set}(p-uniq : (x y : P) → x ≡ y) → (p q : AltDec P) → p ≡ q
  lemm p-uniq (yes a) (yes b) rewrite p-uniq a b = refl
  lemm _ (yes p) (no ¬p) with launder (¬p p); ... | ()
  lemm _ (no ¬p) (yes p) with launder (¬p p); ... | ()
  lemm _ (no _) (no _) = refl

  launder : .⊥ → ⊥
  launder ()

Is there a reason to avoid this, besides irrelevance being
somewhat new and experimental? Should the with-clause
work without introducing the "launder" function?

Brandon