+(*
+let rec i_moves a i on i : Vector move i ≝
+ match i with
+ [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
+ | S j ⇒ vec_cons ? (nth j ? a N) j (i_moves a j)
+ ]. *)
+
+definition vec_moves ≝ λQ,sig,n,a,i.
+ resize_vec … (get_moves Q sig n a) i N.
+
+axiom vec_moves_cons: ∀Q,sig,n,a,j.j < n →
+ vec_moves Q sig n a (S j) =
+ vec_cons ? (get_move Q ? n a j) j (vec_moves Q sig n a j).
+