proposition: Lemma map_map A B C: forall (f:A->B) (g:B->C) n (v : t A n), map g (map f v) = map (fun x => g (f x)) v.
proof: Proof. intros f g n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto. Qed.
imports: VectorDef PeanoNat Eqdep_dec