Problem:
 foldr (\x y. k x y) z nil -> z
 foldr (\x y. k x y) z (cons x xs) -> k x (foldr (\x y. k x y) z xs)
 build (\k z. g (\x y. k x y) z) -> g cons nil
 foldr (\x y. k x y) z (build (\k z. g (\x y. k x y) z)) -> g (\x y. k x y) z

Proof:
 Open