proposition: Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
proof: Proof. intros a v;apply JMeq_eq. apply vector0_is_vnil_aux. trivial. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat