Given:
	
		data Nat = Zero | Succ Nat
		
		data List a = Nil | Cons a (List a)
		
		length Nil = Zero
		length (Cons x xs) = Succ (length xs)
		
		map f Nil = Nil
		map f (Cons x xs) = Cons (f x) (map f xs)

prove that:

		length (map f xs) = length xs
    
    Proof by induction on structure of xs :: List a
    
        case xs = Nil:
        
            length (map f Nil) = length Nil
            
            length Nil = length Nil
            
            QED                                                { ... }
    
        case xs = Cons y ys:
        
        	Assume: length (map f ys) = length ys
        	
        	length (map f (Cons y ys)) = length (Cons y ys)
        	
        	length (Cons (f y) (map f ys)) = ...
        	
        	Succ (length (map f ys)) = length (Cons y ys)
        	
        	Succ (length (map f ys)) = Succ (length ys)
        	
        	length (map f ys) = length ys
        	
        	QED