    (cond
      ;; binder
      (stx/binder? t)
-     (let [[binder [x ty] body] t]
-       ;; 1) try reduction in binding type
-       (let [[ty' red?] (delta-step def-env ty local?)]
-         (if red?
-           [(list binder [x ty'] body) true]
-           ;; 2) try reduction in body
-           (let [[body' red?] (delta-step def-env body local?)]
-             [(list binder [x ty] body') red?]))))
+     (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' red?] (delta-step def-env left local?)]
-       (if red?
-         [[left' right] true]
-         ;; 2) try right reduction
-         (let [[right' red?] (delta-step def-env right local?)]
-           [[left right'] red?])))
+           [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' red?] (delta-step-args def-env args local?)]
-       (if red?
-         [(list* def-name args') red?]
-         (delta-reduction def-env t local?)))
+           [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])))
 

(declare beta-step)

(defn beta-step-args [ts]
  (loop [ts ts, ts' []]
    (if (seq ts)
      (let [[t' red?] (beta-step (first ts))]
        (if red?
          [(vconcat (conj ts' t')
                    (rest ts)) true]
          (recur (rest ts) (conj ts' t'))))
      [ts' false])))

(defn beta-step [t]
  (cond
    ;; binder
    (stx/binder? t)
    (let [[binder [x ty] body] t]
      ;; 1) try reduction in binding type
      (let [[ty' red?] (beta-step ty)]
        (if red?
          [(list binder [x ty'] body) true]
          ;; 2) try reduction in body
          (let [[body' red?] (beta-step body)]
            [(list binder [x ty] body') red?]))))
    ;; application
    (stx/app? t)
    (let [[left right] t
          ;; 1) try left reduction
          [left' red?] (beta-step left)]
      (if red?
        [[left' right] true]
        ;; 2) try beta (if it's a redex)
        (if (stx/lambda? left)
          [(beta-reduction t) true]
          ;; 3) try right reduction
          (let [[right' red?] (beta-step right)]
            [[left right'] red?]))))
    ;; reference
    (stx/ref? t)
    (let [[def-name & args] t
          [args' red?] (beta-step-args args)]
      [(list* def-name args') red?])
    ;; other cases
    :else [t false]))


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

