       (let [[status ts] (parse-terms def-env (rest t) bound)]
         (if (= status :ko)
           [:ko {:msg "Wrong argument" :term t :from ts}]
-          [:ok (conj (conj (into '() ts) def-name) ::stx/ref)])))))
+          [:ok (list* def-name ts)])))))
 
 (example
  (parse-term {'ex {:arity 2}}
              '(ex x :kind) #{'x})
- => '[:ok (:typetheory.syntax/ref ex :kind x)])
-
+ => '[:ok (ex x :kind)])
 
 (defn left-binarize [t]
   (if (< (count t) 2)
     t
-    (loop [s (rest (rest t)), res (list (first t) (second t))]
+    (loop [s (rest (rest t)), res [(first t) (second t)]]
       (if (seq s)
-        (recur (rest s) (list res (first 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))
+ (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)

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

(example
 (parse-binding {} '[x y x :type] #{})

              (not (symbol? (first s)))
              [:ko {:msg "Binding variable is not a symbol" :term v :var (first s)}]
              (reserved-symbol? (first s))
              [:ko {:msg "Wrong binding variable: symbol is reserved" :term v :symbol (first s)}]
              (contains? vars (first s))
              [:ko {:msg "Duplicate binding variable" :term v :var (first s)}]
              :else (recur (rest s) (conj vars (first s)) (conj res [(first s) ty'])))
