proposition: Lemma last_cons A (x : A) y ys : last (y :: ys) x = last ys y.
proof: Proof. generalize dependent x. induction ys using rev_ind; simpl; intros. reflexivity. rewrite !last_rcons. destruct ys; auto. Qed.
imports: Coq.Lists.List Category.Lib.Tactics