[Agda] extending equality

[Sergei Meshveliani]

How do you think, please,
is there possible a simpler expression for  cSym  below?

-------------------------------------------------------------
data Cardinality : Set where  fin      : ℕ → Cardinality
                              infinity : Cardinality
_=c_ : Rel Cardinality _
(fin m)  =c (fin n)  =  m ≡ n
infinity =c infinity =  ⊤
_        =c _        =  ⊥

natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO    -- for ℕ
natSetoid    = DecSetoid.setoid natDecSetoid 
natEquiv     = Setoid.isEquivalence natSetoid 

open IsEquivalence natEquiv renaming 
                          (refl to nRefl; sym to nSym; trans to nTrans)
_≟_ = DecSetoid._≟_ natDecSetoid  

cSym : Symmetric _=c_
cSym {infinity} {infinity} _    =  ⊤.tt
cSym {infinity} {fin _}    x='y =  ⊥-elim x='y
cSym {fin _}    {infinity} x='y =  ⊥-elim x='y
cSym {fin m}    {fin n}    x='y  with m ≟ n
...                            | yes m=n = nSym m=n 
...                            | no m/=n = ⊥-elim $ m/=n x='y 
---------------------------------------------------------------

I hoped for   cSym {fin m}  {.(fin m)} _  =  nRefl
              cSym infinity .infinity  _  =  ⊤.tt

to work - due to the type of the third argument.
Buth all my `dot' variants are not type-checked.

Thanks,

------
Sergei