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. Get busy.