proposition: Lemma Vmap_proj1_sig : forall n (v : vector A n) (Hv : Vforall P v), v = Vmap (@proj1_sig A P) (Vsig_of_forall _ Hv).
proof: Proof. intros n v. elim v. simpl. intro. refl. intros a p w. intro Hrec. simpl. intro Hv. case Hv. intros H1 H2. simpl Vmap. gen (Hrec H2). intro H. apply Vcons_eq_intro; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)