Hi list, Proposition: map f (ys ++ zs) = map f ys ++ map f zs (Haskell, the craft of functional programming, exercise 11.31) Almost every time I'm asked to do (structural) induction over multiple 'things', in this example lists, I don't know how to do it. (I encountered similar difficulties when I worked through chapter 9, see https://github.com/pascal-knodel/haskell-craft/tree/master/Chapter%209 , ex. 9.5 , https://github.com/pascal-knodel/haskell-craft/blob/master/Chapter%209/E%279...). I think my proof in this case isn't formally correct. It feels like it isn't. I would like to do the example with your help, so that I feel a little bit safer. Let's start with the base case. If I have two lists, do I select one, say ys := [] . Only one or one after another? Or both 'parallel'? I could state ys ++ zs := [] too, does it help? I could imagine that the proposition could be expanded to something like map f (l1 ++ l2 ++ ... ++ lN) = map f ys ++ map f zs = map f l1 ++ map f l2 ++ ... ++ map f lN And I could imagine that it is possible to do induction over more than two lists too. What is the reason why we can do it over two 'objects' at the same time? How do I start? Can you explain this to me? Attempt: -- --------------- -- 1. Proposition: -- --------------- -- -- map f (ys ++ zs) = map f ys ++ map f zs -- -- -- Proof By Structural Induction: -- ------------------------------ -- -- -- 1. Induction Beginning (1. I.B.): -- --------------------------------- -- -- -- (Base case 1.) :<=> ys := [] -- -- => (left) := map f (ys ++ zs) -- | (Base case 1.) -- = map f ([] ++ zs) -- | ++ -- = map f zs -- -- -- (right) := map f ys ++ map f zs -- | (Base case 1.) -- = map f [] ++ map f zs -- | map -- = map f zs -- -- -- => (left) = (right) -- -- ✔ -- -- -- 1. Induction Hypothesis (1. I.H.): -- ---------------------------------- -- -- For an arbitrary, but fixed list "ys", the statement ... -- -- map f (ys ++ zs) = map f ys ++ map f zs -- -- ... holds. -- -- -- 1. Induction Step (1. I.S.): -- ---------------------------- -- -- -- (left) := map f ( (y : ys) ++ zs ) -- | ++ -- = map f ( y : ( ys ++ zs ) ) -- | map -- = f y : map f ( ys ++ zs ) -- | (1. I.H.) -- = f y : map f ys ++ map f zs -- | map -- = map f (y : ys) ++ map f zs -- -- -- (right) := map f (y : ys) ++ map f zs -- -- -- => (left) = (right) -- -- -- ?■? (1. Proof) But in this 'proof attempt' only "ys" was considered (1. I.H.). What do I miss? Pascal