proposition: Lemma Vmap_eq_id : forall (A : Type) (f : A->A) n (v : vector A n), Vforall (fun a => f a = a) v -> Vmap f v = v.
proof: Proof. intros. rewrite <- Vmap_id. apply Vmap_eq. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)