module HEqTest where

open import Data.List
open import Relation.Binary.HeterogeneousEquality

data _∈_ {A : Set} : A → List A → Set where
  this : ∀ {x xs} → x ∈ (x ∷ xs)
  next : ∀ {x y xs} → y ∈ xs → 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 ()