 (declare special-step)
 
 (defn special-step-args [def-env ctx ts]
-  (loop [ts ts, ts' []]
+  (loop [ts ts, ts' [], red? false]
     (if (seq ts)
-      (let [[t' red?] (special-step def-env ctx (first ts))]
-        (if red?
-          [(vconcat (conj ts' t')
-                    (rest ts)) true]
-          (recur (rest ts) (conj ts' t'))))
-      [ts' false])))
+      (let [[t' red1?] (special-step def-env ctx (first ts))]
+        (recur (rest ts) (conj ts' t') (or red? red1?)))
+      [ts' red?])))
 
 (defn special-step [def-env ctx t]
   ;; (println "[delta-step] t=" t)

    (stx/binder? t)
    (let [[binder [x ty] body] t]
      ;; 1) try reduction in binding type
      (let [[ty' red?] (special-step def-env ctx ty)]
        (if red?
          [(list binder [x ty'] body) true]
          ;; 2) try reduction in body
          (let [[body' red?] (special-step def-env ctx body)]
            [(list binder [x ty] body') red?]))))
    ;; application
    (stx/app? t)
    (let [[left right] t
          ;; 1) try left reduction
          [left' red?] (special-step def-env ctx left)]
      (if red?
        [[left' right] true]
        ;; 2) try right reduction
        (let [[right' red?] (special-step def-env ctx right)]
          [[left right'] red?])))
    ;; reference
    (stx/ref? t)
    (let [[def-name & args] t
          [args' red?] (special-step-args def-env ctx args)]
      (if red?
        [(list* def-name args') red?]
        (special-reduction def-env ctx t)))
    ;; other cases
    :else [t false]))


   (cond
     ;; binder
     (stx/binder? t)
     (let [[binder [x ty] body] t
           ;; 1) try reduction in binding type
           [ty' red1?] (delta-step def-env ty local?)
           ;; 2) also try reduction in body
           [body' red2?] (delta-step def-env body local?)]
       [(list binder [x ty'] body') (or red1? red2?)])
     ;; application
     (stx/app? t)
     (let [[left right] t
           ;; 1) try left reduction
           [left' lred?] (delta-step def-env left local?)
           ;; 2) also try right reduction
           [right' rred?] (delta-step def-env right local?)]
       [[left' right'] (or lred? rred?)])
     ;; reference
     (stx/ref? t)
     (let [[def-name & args] t
           [args' red1?] (delta-step-args def-env args local?)
           t' (if red1? (list* def-name args') t)
           [t'' red2?] (delta-reduction def-env t' local?)]
       [t'' (or red1? red2?)])
     ;; other cases
     :else [t false])))

