           [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]))
 

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


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

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

(defn instantiate-def [params body args]
  (loop [args args, params params, sub {}]
    (if (seq args)
      (if (empty? params)
        (throw (ex-info "Not enough parameters (please report)" {:args args}))
        (recur (rest args) (rest params) (assoc sub (ffirst params) (first args))))
      (loop [params (reverse params), res body]
        (if (seq params)
          (recur (rest params) (list 'lambda (first params) res))
          (stx/subst res sub))))))

(example
 (instantiate-def '[[x :type] [y :type] [z :type]]
                  '[[x y] z]
                  '((lambda [t :type] t) t1 [t2 t3]))
 => '[[(lambda [t :type] t) t1] [t2 t3]])

(example
 (instantiate-def '[[x :type] [y :type] [z :type] [t :type]]
                  '[[x y] [z t]]
                  '((lambda [t :type] t) t1 [t2 t3]))
 => '(lambda [t' :type] [[(lambda [t :type] t) t1] [[t2 t3] t']]))

(example
 (instantiate-def '[[x :type] [y :type] [z :type]]
                  '[[x y] z]
                  '())
 => '(lambda [x :type] (lambda [y :type] (lambda [z :type] [[x y] z]))))

 (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 (> (count args) (:arity sdef))
            (throw (ex-info "Too many arguments to instantiate definition." {:term t :def-name name :nb-params (count (:arity sdef)) :nb-args (count args)}))
            (if (:parsed-term sdef)
              [(instantiate-def (:params sdef) (:parsed-term sdef) args) true]
              [t false])))))))

(example
