====== Haskell ====== ===== Prove: concat \$ map (map f) xss == map f \$ concat xss ===== prove: concat $ map (map f) xss == map f $ concat xss --------------------------------------------------- case I:xss = []: concat $ map (map f) [] == concat [] == [] map f $ concat [] == map f [] == [] --------------------------------------------------- case II:xss = undefined concat $ map (map f) undefined == concat undefined == undefined map f $ concat undefined == map f undefined == undefined --------------------------------------------------- case III:xss = ys : yss concat $ map (map f) (ys:yss) == concat $ map f ys : map (map f) yss == map f ys ++ (concat $ map (map f) yss) == map f ys ++ (map f $ concat yss) == map f $ ys ++ concat yss == map f $ concat (ys:yss) QED.