On 2012-11-05 13:00, Serge D. Mechveliani wrote: > Finally there appeared a report of that the checker expects Set (max c l) > for ((q * b) ~~ a), and this was a luck. You may want to inspect the constraints (see the Agda menu). -- /NAD