module
Eq
where
infix
70
_≡_
data
_≡_
{
A
:
Set
}
x
:
A
→
Set
where
refl
:
x
≡
x