Issue2925.agda:12,1-20
Rewrite rule  rew  has already been added
when checking the pragma REWRITE rew

———— All done; warnings encountered ————————————————————————

Issue2925.agda:12,1-20
Rewrite rule  rew  has already been added
when checking the pragma REWRITE rew
