Agda-2.6.0: A dependently typed functional programming language and proof assistant

simplifyLevelConstraint c cs turns an c into an equality constraint if it is an inequality constraint and the reverse inequality is contained in cs.