(defun makecases (a terms strict)
  (when terms
    (cons (format nil "~a ~a ~a"
    a
    (if (= strict 1) "<" "<=")
    (car terms))
   (makecases (car terms) (cdr terms) (- strict 1)))))

(defstep trans-ineq (&optional (fnum 1) terms (strict 0))
  (let ((expr (extra-get-formula fnum)))
    (if (is-relation expr t)
 (let ((a (args1 expr))
       (b (args2 expr))
       (myt (if (listp terms) terms (list terms)))
       (casestr (format nil "~{~a~#[~:; AND ~]~}"
          (makecases a
       (append myt (list b))
       strict))))
   (then
    (label "TR" fnum)
    (spread (case casestr)
     ((then (flatten) (assert))
      (then (hide "TR")
     (split 1))))))
      (skip-msg "Not a suitable formula")))
  "" "")