Issue138.agda:6,3-25
Record types are not allowed in mutual blocks