(defun cons-all (e x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      nil
      (cons (cons e (car x))
            (cons-all e (cdr x)))))

(defun combinations (x n)
  (declare (xargs :guard (and (true-listp x)
                              (natp n))))
  (cond
    ((zp n) (list nil))
    ((endp x) nil)
    (t
     (append (cons-all (car x)
                       (combinations (cdr x) (- n 1)))
             (combinations (cdr x) n)))))

(defun comb (n k)
  (cond
    ((zp k) 1)
    ((zp n) 0)
    (t (+ (comb (- n 1) k)
          (comb (- n 1) (- k 1))))))

(defthm len-combinations
  (equal (len (combinations x n))
         (comb (len x) n)))