It is a surprising fact in lambda calculus that lists can be expressed as lambda abstractions. Indeed, the list constructor cons can be written as (x. y. f. f x y). With this definition one can write car as (z. z (x. y. x)) and cdr as (z. z (x. y. y)). Show that using these definitions the usual formulas (car (cons a b)) = a and (cdr (cons a b)) = b are true.