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.