module Data.List.First.Properties {ℓ}{A : Set ℓ} where

open import Data.Product
open import Data.List
open import Data.List.Any
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Empty
open import Data.List.First
open import Data.List.Any.Membership.Propositional

first⟶∈ : ∀ {B : A → Set} {x l} → First B x l → (x ∈ l × B x)
first⟶∈ (here {x = x} p) = here refl , p
first⟶∈ (there x' ¬px f) with (first⟶∈ f)
first⟶∈ (there x' ¬px f) | x∈l , p = there x∈l , p

first-unique : ∀ {P : A → Set}{x y v} → First P x v → First P y v → x ≡ y
first-unique (here x) (here y) = refl
first-unique (here {x = x} px) (there .x ¬px r) = ⊥-elim (¬px px)
first-unique (there x ¬px l) (here {x = .x} px) = ⊥-elim (¬px px)
first-unique (there x' _ l) (there .x' _ r) = first-unique l r