WithoutK5.agda:12,24-28 Cannot eliminate reflexive equation a = a of type A because K has been disabled. when checking that the pattern refl has type _≡_ {_≡_ {A} a a} refl refl