WithoutK3.agda:25,9-13
Cannot eliminate reflexive equation A = A of type Set because K has
been disabled.
when checking that the pattern refl has type _≅_ {A} x {A} y