Last element of list with proof

We have last’ defined like:

last' [x] = x
last' (x:xs) = last' xs (*)

Base case: A list of one element is equal to that element itself.

Inductive step: Assume that last’ (x:xs) returns the last element of the list.
Then, if last’ (x:xs) holds, last’ (y:x:xs) must also hold.

We must show that it holds for y:x:xs.

Set zs = x:xs and obtain:
last’ (y:zs) = (*) = last’ zs = last’ (x:xs) = inductive assumption = last element of the list

So the recursion chops elements from beginning until it reaches one element, which will be the last element from our list.