Prop

EquivRel x,y:. x E y

x,y:. Dec(x E y)

r:(). x,y:. (x r y) (x E y)

h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))

1	4. r: 5. x,y:. (x r y) (x E y) h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))

About: