proposition: Lemma map_append A B: forall (f:A->B) n m (v: t A n) (w: t A m), (map f (v ++ w)) = map f v ++ map f w.
proof: Proof. intros f n m v w. induction v as [|? ? v IHv]. - reflexivity. - cbn. apply f_equal, IHv. Qed.
imports: VectorDef PeanoNat Eqdep_dec