WithoutK-PatternMatchingLambdas1.agda:11,18-22 Cannot eliminate reflexive equation x = x of type A because K has been disabled. when checking that the pattern refl has type x ≡ x