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

                  '(test [a b] c [t (lambda [t] t)]))
 => '[(test [a b] c [t (lambda [t] t)]) false])

(example
 (delta-reduction '{test {:arity 3
                          :params [[x :type] [y :kind] [z :type]]
                          :parsed-term [y (lambda [t :type] [x [z t]])]}}
                  '(test [a b] c))
 => '[(lambda [z :type] [c (lambda [t :type] [[a b] [z t]])]) true])

(defn delta-step [def-env t]
  (cond
    ;; binder
    (stx/binder? t)
    (let [[binder [x ty] body] t]
