(forall (name arg type out f) ((the (Pi name type out) f) (the type arg)) (let name arg (the out (f arg))))
(forall (in out) (-> in out) (Pi _ in out))
(forall (var body arg) ((lambda var body) arg) (let var arg body))

(def _ genslop)
(def succ (the (-> nat nat) 1+))
(def cons (the (Pi A U (Pi B U (-> A (-> B (Pair A B))))) (lambda _ (lambda _ (lambda a (lambda b (pair a b)))))))
(def car  (the (Pi A U (Pi B U (-> (Pair A B) A)))        (lambda _ (lambda _ (lambda p (car' p))))))
(forall (a b) (car' (pair a b)) a)

(def vecnil (the (Pi T U (Vec 0 T)) (lambda _ Vecnil)))

; ordering is bad
(def veccons
    (the (Pi len nat (Pi T U (-> T (-> (Vec len T) (Vec (1+ len) T)))))
        (lambda _ (lambda _ (lambda x (lambda xs (Veccons x xs)))))))

(let sym-nil (vecnil (the U symbol))
(let our-cons-1 ((veccons (the nat 0)) (the U symbol))
(let our-cons-2 ((veccons (succ (the nat 0))) (the U symbol))
((our-cons-2 (the symbol h)) ((our-cons-1 (the symbol i)) sym-nil))
)))