The last element of a list

Define the inductive predicate (last A a l) meaning
l is a list of terms of type A and a is the last item of l

Define a function last_fun of type (list A -> option A) which returns the last element of a list (if it exists).
Then show the consistency between both definitions.

Solution

Look at this file .