RewriteRelationNotSort.agda:7,1-26 a does not have the right type for a rewriting relation because its type does not end in a sort, but in A when checking the pragma BUILTIN REWRITE a