idris-0.9.17.1: test/error001/expected
test002.idr:1:6:Universe inconsistency.
Working on: z
Old domain: Domain 6 6
New domain: Domain 6 5
Involved constraints:
ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}
ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}
ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}