WithoutK1.agda:13,7-11 Cannot eliminate reflexive equation x = x of type A because K has been disabled. when checking that the pattern refl has type x ≡ x