OpenInMutual.agda:9,8-9 Open declarations are not allowed in mutual blocks