[Agda] constructor injectiveness

[Sergei Meshveliani]

People,

I need to program  _≟d_  below,
and do this by introducing con-injective and +injective.
 
Is there possible a simpler expression for _≟d_ ?
Probably injectiveness of constructors like `con' needs to be somehow in
Standard, similarly as PE.cong is in standard (?)

Thanks, 

------
Sergei


-----------------------------------------------------------------------
open import Function using (_∘_; case_of_)
open import Relation.Nullary using (yes; no)
open import Relation.Binary using () renaming (Decidable to Decidable₂)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Nat     using (ℕ; _≟_)

data D : Set where  con : ℕ → D
       	       	    _+_ : D → D → D

con-injective :  ∀ {e e'} → con e ≡ con e' → e ≡ e'
con-injective PE.refl = PE.refl

+injective :  ∀ {x y z u} → (x + y) ≡ (z + u) → x ≡ z × y ≡ u
+injective {x} {y} {.x} {.y} PE.refl = (PE.refl , PE.refl)

_≟d_ : Decidable₂ (_≡_ {A = D})

(con _) ≟d (_ + _) =  no λ()
(_ + _) ≟d (con _) =  no λ()
(con i) ≟d (con j) =  case i ≟ j
                      of \
                      { (yes i≡j) → yes (PE.cong con i≡j)
                      ; (no i≢j)  → no (i≢j ∘ con-injective)
                      }
(x + y) ≟d (z + u) =
           case (x ≟d z , y ≟d u)
           of \
           { (yes x≡z , yes y≡u) → yes (PE.cong₂ _+_ x≡z y≡u)
           ; (no x≢z , _       ) → no (x≢z ∘ proj₁ ∘ +injective)
           ; (_ ,      no y≢u  ) → no (y≢u ∘ proj₂ ∘ +injective)
           }