-- The Agda standard library
-- Properties of coinductive lists and their operations

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

module Codata.Musical.Colist.Properties where

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

    a b : Level
    A : Set a
    B : Set b

∷-injectiveˡ :  {x y xs ys}  (Colist A  x  xs)  y  ys  x  y
∷-injectiveˡ refl = refl

∷-injectiveʳ :  {x y xs ys}  (Colist A  x  xs)  y  ys  xs  ys
∷-injectiveʳ refl = refl