fact: Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with _ , Vector.nil => None | 0 , Vector.cons b _ => Some b | S n', @Vector.cons _ _ p' v' => vector_nth A n' p' v' end.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool