(forall (car' cdr) (car (cons car' cdr)) car')
(forall (car cdr') (cdr (cons car cdr')) cdr')

(forall (a as bs) (++ (cons a as) bs) (cons a (++ as bs)))
(forall (bs)      (++ () bs) bs)

(forall (f acc)      (foldr f acc ()) acc)
(forall (f acc x xs) (foldr f acc (cons x xs)) (foldr f (app f acc x) xs))

(forall (x xs) (snoc x xs) (++ xs (cons x ())))

(def (reverse ()) ())
(forall (x xs) (reverse (cons x xs)) (snoc x (reverse xs)))

(forall (bindings body) (@ bindings body) (lambda-like lambda bindings body))
(forall (var body arg) ((lambda var body) arg) (let var arg body))

(forall (lam bindings body)
 (lambda-like' lam bindings body)
(unquote
(foldr
(@ (acc' x')
(quote (lam x' acc'))
)
body
(reverse (quote bindings))
)
)
)

(lambda-like' -> (a b c) d)