proposition: Theorem zero_nil : forall (A:Set) (v:Vector.t A 0), v = Vector.nil.
proof: Proof. intros. change (Vector.nil (A:=A)) with (Vid _ 0 v). apply Vid_eq. Defined.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat