E:(Prop). (EquivRel x,y:. x E y) & (x,y:. Dec(x E y)) (h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n))))

1	1. E: Prop 2. EquivRel x,y:. x E y 3. x,y:. Dec(x E y) h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))

About: