proposition: Theorem last_fun_correct_R : forall (a:A) (l:list A), last_fun l = Some a -> last a l.
proof: Proof. intros a l ; induction l as [ |a0 l0 IHl0]; simpl. - discriminate. - destruct l0. + injection 1;intros;subst a0;auto. + intro e; simpl; auto. Qed.
imports: List