proposition: Lemma append_inj {A} : forall {n m : nat} (v v' : t A n) (w w' : t A m), v ++ w = v' ++ w' -> v = v' /\ w = w'.
proof: Proof. intros n m v v' w w' E%(f_equal (splitat _)). apply pair_equal_spec. now rewrite <- !splitat_append. Qed.
imports: VectorDef PeanoNat Eqdep_dec