:set-state-ok t

(defun pick-random-element (xs state)
   (mv-let (idx state)
           (random$ (len xs) state)
      (mv (nth idx xs) state)))