Can someone provide the induction-case proof of the following identity: foldl (-) ((-) x y) ys = (foldl (-) x ys) - y If foldl is defined as usual: foldl :: (b -> a -> b) -> b -> [a] -> b foldl f e [] = e foldl f e (x : xs) = myFoldl f (f e x) xs The first two cases, _|_ and [], are trivial. Here's my best attempt at the (y : ys) case (the left and right sides reduce to expressions that are obviously equal, but I don't know how to show it): Case (y : ys). Left-side reduction: foldl (-) ((-) x y) (y : ys) = {second equation of "foldl"} foldl (-) ((-) ((-) x y) y) ys = {notation} foldl (-) ((-) (x - y) y) ys = {notation} foldl (-) ((x - y) - y) ys = {arithmetic} foldl (-) (x - 2 * y) ys Right-side reduction: (foldl (-) x (y : ys)) - y = {second equation of "foldl"} (foldl (-) ((-) x y) ys) - y = {induction hypothesis: foldl (-) ((-) x y) ys = (foldl (-) x ys) - y} ((foldl (-) x ys) - y) - y = {arithmetic} (foldl (-) x ys) - 2 * y Thanks as always. _________________________________________________________________ Express your personality in color! Preview and select themes for Hotmail®. http://www.windowslive-hotmail.com/LearnMore/personalize.aspx?ocid=TXT_MSGTX...