{-# OPTIONS --without-K --show-implicit #-}

module WithoutK9 where

module Eq {A : Set} (x : A) where

  data _≡_ : A → Set where
    refl : _≡_ x

open Eq

module Bad {A : Set} {x : A} where

  module E = Eq x

  weak-K : {y : A} (p q : E._≡_ y) (α β : p ≡ q) → α ≡ β
  weak-K refl .refl refl refl = refl