1. The problem statement, all variables and given/known data Prove by finite list induction ∀xs:: [a]. map (\x -> x) xs = xs 2. Relevant equations map f [ ] = [ ] map f (x : xs) = (f x) : map f xs 3. The attempt at a solution The list induction principle to prove a finite lists of type a is [P([ ])^ ∀x :: a. ∀xs :: [a]. P(xs) => P(x : xs) => ∀ys :: [a].P(ys) So, to show ∀ys :: [a]. P(ys) we need to show two things i.) P([ ]) ii.) ∀x :: a. ∀xs :: [a]. P(xs) => P(x : xs) the i) part is really easy, it's just a base case but I am totally stomped on how to even go about proving the ii) part. I would like a guidance on this. Do I assume an arbitrary k of a newly list (that is previously constructed) and try to do an inductive proof? I don't know, I'm really lost.