A useful lemma for the [last] function, to reduce
last (x::l) = Some y to
last l = Some y whenever
x ≠ y.
This is useful since using
last_cons leaves us with
match last l with | Some y0 => Some y0 | None => Some x end = Some y
which only reduces through a subgoal.