proposition: Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
proof: Proof. intros A v;inversion v. Abort. Require Import JMeq. Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> JMeq v (Vector.nil A). Proof. destruct v. auto. intro; discriminate. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat