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

simplifyLevelConstraint n c cs turns an c into an equality constraint if it is an inequality constraint and the reverse inequality is contained in cs. Number n is the length of the context c is defined in.