WithoutK-PatternSynonyms2.agda:13,14-17 Cannot eliminate reflexive equation x₁ = x₁ of type A because K has been disabled. when checking that the pattern refl x has type x ≡ x