Given:
	
		data List a = Nil | Cons a (List a)
				
		map f Nil = Nil
		map f (Cons x xs) = Cons (f x) (map f xs)

		append Nil ys = ys
		append (Cons x xs) ys = Cons x (append xs ys)

prove that:

		map f (append as bs) = append (map f as) (map f bs)
    
    Proof by induction on structure of as :: List a
    
        case as = Nil:
        
            map f (append Nil bs) = append (map f Nil) (map f bs)
            
            map f bs = append Nil (map f bs)
            
            map f bs = map f bs
            
            QED                                                { ... }
    
        case as = Cons c cs:
        
        	Assume: map f (append cs bs) = append (map f cs) (map f bs)
        	
        	Prove: map f (append (Cons c cs) bs) = append (map f (Cons c cs)) (map f bs)
        	
        	map f (Cons c (append cs bs)) = ...
        	
        	Cons (f c) (map f (append cs bs)) = ...
        	
        	Cons (f c) (map f (append cs bs)) = append (map f (Cons c cs)) (map f bs)
        	
        	Cons (f c) (map f (append cs bs)) = append (Cons (f c) (map f cs)) (map f bs)
        	
        	Cons (f c) (map f (append cs bs)) = Cons (f c) (append (map f cs) (map f bs))
        	
        	map f (append cs bs) = append (map f cs) (map f bs)
        	
        	QED