proposition: Theorem last_same : forall {A:Type} (a b:A) (l1 l2:list A), l1 ++ a :: nil = l2 ++ b :: nil -> l1 = l2 /\ a = b.
proof: Proof. intros A a b l1 l2 H. assert (e: a :: rev l1 = b :: rev l2). - repeat rewrite <- rev_unit; now rewrite H. - injection e; intros H1 H2; split; auto. rewrite <- (rev_involutive l1), H1; apply rev_involutive. Qed.
imports: List Arith