{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Membership.Propositional {a} {A : Set a} where
open import Data.Vec.Base using (Vec)
open import Data.Vec.Relation.Unary.Any using (Any)
open import Relation.Binary.PropositionalEquality.Core using (subst)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)
import Data.Vec.Membership.Setoid as SetoidMembership
open SetoidMembership (setoid A) public hiding (lose)
lose : ∀ {p} {P : A → Set p} {x n} {xs : Vec A n} → x ∈ xs → P x → Any P xs
lose = SetoidMembership.lose (setoid A) (subst _)