    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties, related to reflexive transitive closures, that rely on
    -- the K rule
    ------------------------------------------------------------------------

    {-# OPTIONS --with-K --safe #-}

    module
      Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK
      where

    open import Function.Base using (_∋_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; _◅_)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

    ------------------------------------------------------------------------
    -- Equality

    module _ {i t} {I : Set i} {T : Rel I t} {i j k} {x y : T i j} {xs ys}
      where

      ◅-injectiveˡ : (Star T i k ∋ x ◅ xs) ≡ y ◅ ys → x ≡ y
      ◅-injectiveˡ refl = refl

      ◅-injectiveʳ : (Star T i k ∋ x ◅ xs) ≡ y ◅ ys → xs ≡ ys
      ◅-injectiveʳ refl = refl