Dear Agda developers,
When the level does not fit, the checker
(in Agda of darcs August 2013)
reports of level expressions like
suc l' ⊔ (suc l ⊔ suc c) (e)
Probably it is better to simplify such expressions.
For example,
(e) --> suc (l' ⊔ l ⊔ c)
Regards,
------
Sergei