member-heq.agda

{-# OPTIONS --without-K #-}

open import Data.List
open import Data.Sum
open import Relation.Binary.PropositionalEquality

module _ (A : Set) where

  data _∈_ (a : A) : List A → Set where
    here  : ∀ {as} → a ∈ (a ∷ as)
    there : ∀ {a' as} → a ∈ as → a ∈ (a' ∷ as)

  del : ∀ {a} as → a ∈ as → List A
  del (a ∷ as) here      = as
  del (a ∷ as) (there p) = a ∷ del as p

  ∈-heq : ∀ {a a' as} → (p : a ∈ as) → a' ∈ as → (a' ∈ del as p) ⊎ (a ≡ a')
  ∈-heq here      here      = inj₂ refl
  ∈-heq here      (there q) = inj₁ q
  ∈-heq (there p) here      = inj₁ here
  ∈-heq (there p) (there q) with ∈-heq p q
  ... | inj₁ q' = inj₁ (there q')
  ... | inj₂ eq = inj₂ eq

  ∈-heq-eq :
    ∀ {a a' as eq}(p : a ∈ as)(q : a' ∈ as) → ∈-heq p q ≡ inj₂ eq → subst (_∈ as) eq p ≡ q
  ∈-heq-eq here      here      refl = refl
  ∈-heq-eq here      (there q) ()
  ∈-heq-eq (there p) here      ()
  ∈-heq-eq (there p) (there q) r with ∈-heq p q | inspect (∈-heq p) q
  ∈-heq-eq (there p) (there q) ()   | inj₁ _    | _
  ∈-heq-eq (there p) (there q) refl | inj₂ refl | [ eq ] = cong there (∈-heq-eq p q eq)