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