proposition: Lemma to_list_last A n (v : t A (S n)) d: last v = List.last (to_list v) d.
proof: Proof. apply rectS with (v:=v); [reflexivity|]. intros a k u IH. rewrite to_list_cons. simpl List.last. now rewrite <- IH, (eta u). Qed.
imports: VectorDef PeanoNat Eqdep_dec