[Agda] Problem proving inequality with HeterogeneousEquality

[Shin-Cheng Mu]

Hi,

The following is a typical definition of a membership
relation --- x ∈ xs indicates that x is a member of the
list xs:

 data _∈_ {A : Set} : A → List A → Set where
   this : ∀ {x xs} → x ∈ (x ∷ xs)
   next : ∀ {x y xs} → y ∈ xs → y ∈ (x ∷ xs)

I encountered a question: how do I prove that "this",
does not equal "next"?

Since they might not have the same type, I need 
HeterogeneousEquality. In the following attempt,
"this", with implicit arguments, has type x ∈ (x ∷ xs),
while "next" has type y ∈ (x ∷ xs):

 this≇next : ∀ {A} {x y : A} {xs}
           → (y∈xs : y ∈ xs)
           → this {x = x} {xs} ≇ next {x = x} {y} {xs} y∈xs
 this≇next y∈xs ()

This attempt fails, however. Agda reports the error:

 Failed to solve the following constraints:
   Is empty: this ≅ next y∈xs

How do I convince Agda that "this" is not "next"?

The Agda version is 2.6.1. I have attached the 
simple test file below.

Thank you!

sincerely,
Shin


-------------- next part --------------
A non-text attachment was scrubbed...
Name: HEqTest.agda
Type: application/octet-stream
Size: 405 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200521/ad28998e/attachment.obj>
-------------- next part --------------