(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 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 our-car ((car (the U nat)) (the U symbol)))
(((((cons (the U nat)) (the U symbol)) (the nat 0)) (the symbol hi)))