Hopefully this is just about on topic enough.. (Oh and it's not home work, I just can't bring myself to let it go!) Taken from "Simon Thompson: Type Theory and Functional Programming" Section 1.1 Exercise 1.3 Question: Give a proof of (A => (B => C)) => ((A /\ B) => C). Now I can easily perform (and verify, it's given earlier in the section) the proof of implication with the terms flipped around: ((A /\ B) => C) => (A => (B => C)) Thus: [A]2 [B]1 ----------- (/\ I) [(A /\ B) => C]3 A /\ B ---------------------------------------- (=> E) C --------- (=> I) 1 B => C ------------------ (=> I) 2 A => (B => C) --------------------------- (=> I) 3 ((A /\ B) => C) => (A => (B => C)) My problem arrives finding a solution to the exercise question, my approach is to basically run the above proof backwards. Thus: A => (B => C) A --------------------- (=> E) B B => C --------------------- (=> E) C Now at this point I thought "aha, I can use (=> I) to introduce (A /\ B)" and get: --------------------- (=> I) 1 (A /\ B) => C But here I am only entitled to discharge (A /\ B) in the preceding proof and not A and B on their own. What proof which would allow me to discharge my assumptions A and B? I can see in my head how it makes perfect sense, but can't jiggle a way to do it using only the given derivations. Many thanks, Dave