The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

Or even shorter ;-)

Require Import Vector.
Require Import ArithRing.

Goal match mult_n_O 0 in (_ = y) return (t (option nat) y) with
   | eq_refl => nil (option nat)
   end = nil (option nat).
Proof.
  apply trans_equal with (Vector.const (@None nat) (0 * 0)); auto.
  now destruct (mult_n_O O).
Qed.