proposition: Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v.
proof: Proof. intros a n v; induction v as [|? ? v IHv]; intros m w le. - reflexivity. - simpl. apply f_equal, IHv. Qed.
imports: VectorDef PeanoNat Eqdep_dec