PrimitiveInMutual.agda:10,13-58 Primitive declarations are not allowed in mutual blocks