    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some code related to transitive closures that relies on the K rule
    ------------------------------------------------------------------------

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

    module Relation.Binary.Construct.Closure.Transitive.WithK where

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

    module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where

     ∼⁺⟨⟩-injectiveˡ : ∀ {x y z} {p r : x [ _∼_ ]⁺ y} {q s} →
                       (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → p ≡ r
     ∼⁺⟨⟩-injectiveˡ refl = refl

     ∼⁺⟨⟩-injectiveʳ : ∀ {x y z} {p r : x [ _∼_ ]⁺ y} {q s} →
                       (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → q ≡ s
     ∼⁺⟨⟩-injectiveʳ refl = refl