proposition: Theorem last_fun_correct : forall (a:A) (l:list A), last a l -> last_fun l = Some a.
proof: Proof. intros a l H; induction H as [| b l H IH]. - reflexivity. - destruct l; simpl in *. + discriminate IH. + assumption. Qed.
imports: List