------------------------------------------------------------------------
-- The Agda standard library
--
-- Data.List.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.Membership.Propositional {a} {A : Set a} where
 
open import Data.List.Relation.Unary.Any using (Any)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp; subst)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
import Data.List.Membership.Setoid as SetoidMembership
 
------------------------------------------------------------------------
-- Re-export contents of setoid membership
 
open SetoidMembership (setoid A) public hiding (lose)
 
------------------------------------------------------------------------
-- Different members
 
infix  _≢∈_
 
_≢∈_ : ∀ {x y : A} {xs} → x ∈ xs → y ∈ xs → Set _
_≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs
 
------------------------------------------------------------------------
-- Other operations
 
lose : ∀ {p} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
lose = SetoidMembership.lose (setoid A) (resp _)