proposition: Lemma Vnth_map : forall n (v : vector A n) i (H : i < n), Vnth (Vmap v) H = f (Vnth v H).
proof: Proof. intros n. elim n. intros v i H. exfalso. apply (Nat.nlt_0_r H). clear n. intros n Hrec v i. case i. intro. rewrite (VSn_eq v). simpl. refl. clear i. intros i Hi. rewrite (VSn_eq v). simpl. apply (Hrec (Vtail v) i (NatCompat.lt_S_n Hi)). Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)