  (concat [1 2 3] [4 5 6]) => [1 2 3 4 5 6])
 
 (defn parse-binder-term [def-env binder t bound]
-  (if (not= (count t) 3)
-    [:ko {:msg (str "Wrong " binder " form (expecting 3 arguments)") :term t :nb-args (count t)}]
+  (if (< (count t) 3)
+    [:ko {:msg (str "Wrong " binder " form (expecting at least 3 arguments)") :term t :nb-args (count t)}]
     (let [[status bindings] (parse-binding def-env (second t) bound)]
       (if (= status :ko)
         [:ko {:msg (str "Wrong bindings in " binder " form") :term t :from bindings}]
         (let [bound' (reduce (fn [res [x _]]
                                (conj res x)) #{} bindings)]
-          (let [[status body] (parse-term def-env (nth t 2) bound')]
-            (if (= status :ko)
-              [:ko {:msg (str "Wrong body in " binder " form") :term t :from body}]
-              (loop [i (dec (count bindings)), res body]
-                (if (>= i 0)
-                  (recur (dec i) (list binder (bindings i) res))
-                  [:ok res])))))))))
+          (let [body (if (= (count t) 3)
+                       (nth t 2)
+                       (rest (rest t)))]
+            (let [[status body] (parse-term def-env body bound')]
+              (if (= status :ko)
+                [:ko {:msg (str "Wrong body in " binder " form") :term t :from body}]
+                (loop [i (dec (count bindings)), res body]
+                  (if (>= i 0)
+                    (recur (dec i) (list binder (bindings i) res))
+                    [:ok res]))))))))))
 
 (defn parse-lambda-term [def-env t bound]
   (parse-binder-term def-env 'lambda t bound))

        [:ok (left-binarize ts)]))))

(example
 (parse-term {} '(x y) '#{x y}) => '[:ok (x y)])

(example
 (parse-term {} '(x y z) '#{x y z}) => '[:ok ((x y) z)])

      (let [[status ts] (parse-terms def-env (rest t) bound)]
        (if (= status :ko)
          [:ko {:msg "Wrong argument" :term t :from ts}]
          [:ok (list* def-name ts)])))))

(example
 (parse-term {'ex {:arity 2}}
             '(ex x :kind) #{'x})
 => '[:ok (ex x :kind)])

(defn left-binarize [t]
  (if (< (count t) 2)
    t
    (loop [s (rest (rest t)), res [(first t) (second t)]]
      (if (seq s)
        (recur (rest s) [res (first s)])
        res))))

(example
 (left-binarize '(a b)) => '[a b])

(example
 (left-binarize '(a b c)) => '[[a b] c])

(example
 (left-binarize '(a b c d e)) => '[[[[a b] c] d] e])

(defn parse-application-term [def-env t bound]
  (if (< (count t) 2)
