   (contains? #{'lambda 'λ} t))
 
 (defn product-kw? [t]
-  (contains? #{'prod 'forall '∀} t))
+  (contains? #{'prod 'pi 'Π 'forall '∀} t))
+
+(defn arrow-kw? [t]
+  (contains? #{'imply '--> '-> '=> '==> '→ '➝ '⟶ '⟹} t))
 
 (declare parse-lambda-term
          parse-product-term
+         parse-arrow-term
          parse-defined-term
          parse-application-term)
 

    (cond
      (lambda-kw? (first t)) (parse-lambda-term def-env t bound)
      (product-kw? (first t)) (parse-product-term def-env t bound)
      (contains? def-env (first t)) (parse-defined-term def-env t bound)
      :else (parse-application-term def-env t bound))))



(defn parse-lambda-term [def-env t bound]
  (parse-binder-term def-env 'lambda t bound))

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