../../Task/Pick-random-element/ACL2