Issue260b.agda:5,8-9 Duplicate definition of module R. Previous definition of module R at Issue260b.agda:4,8-9 when scope checking the declaration record R where