module Issue835 where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate
  A : Set
  x y : A

F : x ≡ y → Set
F ()