[Agda] weird error with 'with'

[Samuel Bronson]

I get this error in Term.agda from the darcs repository
http://naesten.dyndns.org:8080/repos/agda-lambda/ :

/home/naesten/hacking/haskell/proofs/lambda/Term.agda:67,7-13
i + j != i of type ℕ
when checking that the pattern ≡-refl has type
.Relation.Binary.Core._≡_ (i + j + j') (i + (j + j'))

P.S. Does anyone know how to get GNU Emacs 21 to copy/paste Unicode
correctly under X? I had to manually insert the correct characters
here instead of the gibberish that I got when I pasted into gmail in
iceweasel... one problem I don't have using emacs in a terminal ;-).