               num (count body)]
           (case (compare (count args) num)
             ;; curry
-            1 (-> (ev term env)
+            1 (-> (ev term vars env)
                   (Forall. (subvec args num))
                   (Form. (reduce disj vars (keys env))))
             ;; beta-reduce
-            0 (as-> (ev term env) term
+            0 (as-> (ev term vars env) term
                 (if (expr? term)
                   (Form. term (reduce disj vars (keys env)))
                   term))
             (throw (ex-info "arity error" {:args args :vals body}))))
-        (Beta. sexp))))
+        (if (seq vars)
+          (Form. (Beta. sexp) vars)
+          (apply head body)))))
 
   Forall
-  (ev [{:keys [term args]} env]
+  ;; - form forall
+  (ev [{:keys [term args]} vars env]
     (let [env  (reduce dissoc env args) ; evalutes term if necessary
-          term (cond-> term (seq env) (ev env))]
-      (if (and (form? term) (forall? (:expr term)))
-        (as-> (:expr term) expr ; uncurries
-          (assoc expr :args (into args (:args expr))))
-        (Forall. term args))))
-
-  Object
-  (fv [this] #{})
-  (ev [this env] this)
-
-  nil
-  (fv [this] #{})
-  (ev [this env] this))
+          term (cond-> term (seq env) (ev vars env))]
+      (if (form? term)
+        (if (forall? (:expr term))
+          ;; uncurries
+          (as-> term [{{:keys [term args']} :expr vars :vars}]
+            (Form. (Forall. term (into args args'))
+                   (reduce disj vars args)))
+          (Form. (Forall. term args) (reduce disj (:vars term) args)))
+        (Form. (Forall. term args) #{}))))
+
+  Object (ev [this _ _] this)
+  nil    (ev [this _ _] this))
 
 (defn ?%
   "takes a term and interleaving var-terms and values, (partially)

;; vars = set var
;; args = vec var

;; term = form | var | val
;; form = expr & vars
;; expr = beta | forall
;;
;; expr are always wrapped in form
;; vars only reduces during evaluation
;;
;; val    => val
;; var    => val | var
;; form   => form | var | val
;; beta   => form | beta | var | val
;; forall => forall

(defrecord Var    [name])         (defn var?    [x] (instance?  Var    x))
(defrecord Form   [expr vars])    (defn form?   [x] (instance?  Form   x))
(defrecord Beta   [sexp])         (defn beta?   [x] (instance?  Beta   x))
(defrecord Forall [term args])    (defn forall? [x] (instance?  Forall x))
(defprotocol Expr)                (defn expr?   [x] (satisfies? Expr   x))
(extend-protocol Expr Beta Forall)

(defprotocol Term
  "

  fv

  ev

  - substitutes all keys in expr to vals in env (: map var val)
  - beta reduces a term whose expr has a Forall as head

  "
  (fv [this])
  (ev [this env]))

(extend-protocol Term

  Var
  (fv [this] #{this})
  (ev [this env] (env this this))

  Form
  (fv [this] (:vars this))
  (ev [{:keys [expr vars]} env]
    (let [;; evaluates expr if necessary
          term (if (some vars (keys env)) (ev expr env) expr)
          vars (if (form? term) (:vars term) (reduce disj vars (keys env)))
          term (if (form? term) (:expr term) term)
          ;; now term is not a form
          term (if (and (beta? term) (empty? vars))
                 (as-> (:sexp term) [head & body]
                   (apply head body))
                 term)]
      (if (expr? term)
        (Form. term vars)
        term)))

  Beta
  (ev [this env]
    (as-> (:sexp this) [head & body :as sexp]
      ;; evalutes sexp if necessary
      (cond->> sexp (seq env) (map #(ev % env)))
      (if (and (form? head) (forall? (:expr head)))
        (let [{:keys [expr vars]} head
              {:keys [term args]} expr

  )

;; todo
;; - fix (keys env)
;; - test how to replace var using env
