9.4.2 - proof by induction over xs

Induction base:
    Suppose xs = []. Then we have:
    
    flatten (map (map f) xs)                    // assumption xs = []
    = flatten (map (map f) [])                  // definition of map, rule 3
    = flatten []                                // definition of flatten, rule 5
    = []                                        // definition of map, rule 3
    = map f []                                  // definition of flatten, rule 5
    = map f (flatten [])                        // assumption xs = []
    = map f (flatten xs).

Induction step:
    Suppose flatten (map (map f) xs) = map f (flatten xs) for certain xs of finite length (induction hypothesis). Then we have:
    
    flatten (map (map f) [x:xs])                // definition of map, rule 4
    = flatten [map f x : map (map f) xs]        // definition of flatten, rule 6
    = (map f x) ++ flatten (map (map f) xs)     // induction hypothesis: assumption flatten (map (map f) xs) = map f (flatten xs)
    = (map f x) ++ (map f (flatten xs))         // by 9.4.1
    = map f (x ++ (flatten xs))                 // definition of flatten, rule 6
    = map f (flatten [x:xs]).

By the principle of induction we have now proven that flatten (map (map f) xs) = map f (flatten xs) for any list of finite length xs.