{-# OPTIONS --safe #-}

module ThisNext where

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

variable
  A : Set
  x y : A
  xs : List A

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

∈-to-ℕ : x ∈ xs → ℕ
∈-to-ℕ this = zero
∈-to-ℕ (next x∈xs) = suc (∈-to-ℕ x∈xs)

this≇next : (x∈xs : x ∈ xs) → this ≇ next x∈xs
this≇next _ t≡n with cong ∈-to-ℕ t≡n
this≇next _ t≡n | ()