           [args' red?] (reduce (fn [[res red?] arg]
                                  (let [[arg' red?'] (delta-step def-env arg)]
                                    [(conj res arg') (or red? red?')])) [[] false] args)]
-      [(list* def-name args') red?])
+      (if red?
+        [(list* def-name args') red?]
+        (delta-reduction def-env t)))
     ;; other cases
     :else [t false]))
 

;; ## Delta-reduction (unfolding of definitions)
;;}

(defn delta-reduction [def-env t]
  (if (not (stx/ref? t))
    (throw (ex-info "Cannot delta-reduce: not a reference term." {:term t}))
    (let [[name & args] t]
      (if (not (get def-env name))
        (throw (ex-info "No such definition" {:term t :def-name name}))
        (let [sdef (get def-env name)]
          (if (not= (count args) (:arity sdef))
            (throw (ex-info "Wrong arity for definition." {:term t :def-name name :expected-arity (:arity sdef)}))
            (if (:parsed-term sdef)
              [(stx/subst (:parsed-term sdef) (zipmap (map first (:params sdef)) args)) true]
              [t false])))))))

(example

;;{
;; ## Normalization (up-to beta/delta)
;;}

(defn normalize
  ([t] (normalize {} t))
