@@ -169,7 +169,8 @@ implementation DecEq Int where
169169 False => No primitiveNotEq
170170 where primitiveEq : x = y
171171 primitiveEq = really_believe_me (Refl {x})
172− postulate primitiveNotEq : x = y -> Void
172+ primitiveNotEq : x = y -> Void
173+ primitiveNotEq = really_believe_me (id {a = x = y})
173174
174175--------------------------------------------------------------------------------
175176-- Char
@@ -181,7 +182,8 @@ implementation DecEq Char where
181182 False => No primitiveNotEq
182183 where primitiveEq : x = y
183184 primitiveEq = really_believe_me (Refl {x})
184− postulate primitiveNotEq : x = y -> Void
185+ primitiveNotEq : x = y -> Void
186+ primitiveNotEq = really_believe_me (id {a = x = y})
185187
186188--------------------------------------------------------------------------------
187189-- Integer
@@ -193,7 +195,8 @@ implementation DecEq Integer where
193195 False => No primitiveNotEq
194196 where primitiveEq : x = y
195197 primitiveEq = really_believe_me (Refl {x})
196− postulate primitiveNotEq : x = y -> Void
198+ primitiveNotEq : x = y -> Void
199+ primitiveNotEq = really_believe_me (id {a = x = y})
197200
198201--------------------------------------------------------------------------------
199202-- String
@@ -205,7 +208,8 @@ implementation DecEq String where
205208 False => No primitiveNotEq
206209 where primitiveEq : x = y
207210 primitiveEq = really_believe_me (Refl {x})
208− postulate primitiveNotEq : x = y -> Void
211+ primitiveNotEq : x = y -> Void
212+ primitiveNotEq = really_believe_me (id {a = x = y})
209213
210214--------------------------------------------------------------------------------
211215-- Ptr
@@ -217,7 +221,8 @@ implementation DecEq Ptr where
217221 False => No primitiveNotEq
218222 where primitiveEq : x = y
219223 primitiveEq = really_believe_me (Refl {x})
220− postulate primitiveNotEq : x = y -> Void
224+ primitiveNotEq : x = y -> Void
225+ primitiveNotEq = really_believe_me (id {a = x = y})
221226
222227--------------------------------------------------------------------------------
223228-- ManagedPtr
@@ -229,4 +234,5 @@ implementation DecEq ManagedPtr where
229234 False => No primitiveNotEq
230235 where primitiveEq : x = y
231236 primitiveEq = really_believe_me (Refl {x})
232− postulate primitiveNotEq : x = y -> Void
237+ primitiveNotEq : x = y -> Void
238+ primitiveNotEq = really_believe_me (id {a = x = y})