proposition: Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m), splitat n (v ++ w) = (v, w).
proof: Proof. intros n m v w. induction v as [|a n v IH]. - reflexivity. - cbn. now rewrite IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec