This is another proof-layout question, this time from Bird 1.4.7. We're asked to define the functions curry2 and uncurry2 for currying and uncurrying functions with two arguments. Simple enough: curry2 :: ((a, b) -> c) -> (a -> (b -> c))curry2 f x y = f (x, y) uncurry2 :: (a -> (b -> c)) -> ((a, b) -> c)uncurry2 f (x, y) = f x y The following two assertions are obviously true theorems, but how are the formal proofs laid out? 1. curry2 (uncurry2 f) x y = f x y 2. uncurry2 (curry 2 f) (x, y) = f (x, y) _________________________________________________________________ The New Busy is not the too busy. Combine all your e-mail accounts with Hotmail. http://www.windowslive.com/campaign/thenewbusy?tile=multiaccount&ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_4