module Eq where

infix 70 _≡_

data _≡_ {A : Set} x : A  Set where
  refl : x  x