@@ -187,30 +187,30 @@ instance DecEq a => DecEq (Vect n a) where
187187--------------------------------------------------------------------------------
188188
189189instance DecEq Int where
190− decEq x y = if x == y then Yes (believe_me (x = x))
191− else No (believe_me _|_)
190+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
191+ else No (really_believe_me _|_)
192192
193193--------------------------------------------------------------------------------
194194-- Char
195195--------------------------------------------------------------------------------
196196
197197instance DecEq Char where
198− decEq x y = if x == y then Yes (believe_me (x = x))
199− else No (believe_me _|_)
198+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
199+ else No (really_believe_me _|_)
200200
201201--------------------------------------------------------------------------------
202202-- Integer
203203--------------------------------------------------------------------------------
204204
205205instance DecEq Integer where
206− decEq x y = if x == y then Yes (believe_me (x = x))
207− else No (believe_me _|_)
206+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
207+ else No (really_believe_me _|_)
208208
209209--------------------------------------------------------------------------------
210210-- Float
211211--------------------------------------------------------------------------------
212212
213213instance DecEq Float where
214− decEq x y = if x == y then Yes (believe_me (x = x))
215− else No (believe_me _|_)
214+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
215+ else No (really_believe_me _|_)
216216