proposition: Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A (n+m)), splitat n vw = (v, w) -> vw = v ++ w.
proof: Proof. intros n m v w vw E. assert (v = fst (splitat n vw)) as -> by now rewrite E. assert (w = snd (splitat n vw)) as -> by now rewrite E. clear E. induction n as [|n IH]. - reflexivity. - cbn. specialize (IH (tl vw)). destruct (splitat n (tl vw)) as [??]. rewrite (eta vw). cbn. apply f_equal, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec