[Agda] Problem proving inequality with HeterogeneousEquality

[Roman]

The answer to a problem with heterogeneous equality is nearly always
"don't use heterogeneous equality".

I use what I call "heteroindexed equality", see
https://lists.chalmers.se/pipermail/agda/2016/009069.html

It allows to directly express the thing that you want:

open import Data.List.Base
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Empty

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

[_]_≅_ : ∀ {X : Set} {x y} → (Z : X → Set) → Z x → Z y → Set
[_]_≅_ {x = x} {y} Z a b = (x , a) ≡ (y , b)

this≇next : ∀ {A} {x y : A} {xs}
          → (y∈xs : y ∈ xs)
          → [ _∈ (x ∷ xs) ] this {x = x} {xs} ≅ next {x = x} {y} {xs} y∈xs
          → ⊥
this≇next y∈xs ()