------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive lists where all elements satisfy a predicate
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module Codata.Musical.Colist.Relation.Unary.All.Properties where

open import Codata.Musical.Colist.Base
open import Codata.Musical.Colist.Relation.Unary.All
open import Codata.Musical.Notation
open import Function.Base using (_∋_)
open import Level using (Level; _⊔_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Unary using (Pred)

private
  variable
    a b p : Level
    A : Set a
    B : Set b
    P : Pred A p

∷-injectiveˡ : ∀ {x xs px qx pxs qxs} →
               (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → px ≡ qx
∷-injectiveˡ refl = refl

∷-injectiveʳ : ∀ {x xs px qx pxs qxs} →
               (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → pxs ≡ qxs
∷-injectiveʳ refl = refl