proposition: Lemma last_app_cons A (x : A) xs y ys : last (xs ++ y :: ys) x = last (y :: ys) x.
proof: Proof. generalize dependent y. generalize dependent xs. induction ys using rev_ind; simpl; intros. apply last_rcons. rewrite last_rcons. rewrite app_comm_cons. rewrite app_assoc. rewrite last_rcons. destruct ys; auto. Qed.
imports: Coq.Lists.List Category.Lib.Tactics