proposition: Lemma split' {X : Type} : forall {m n} (xs : vector X (Peano.plus m n)), Split m n xs.
proof: Proof. fix IH 3. intros m n xs. eassert ?[ty]. refine (match xs as xs' in @t _ k return (match xs' as xs'' in vector _ n' return Type with | nil => ((0, nil) = (Peano.plus m n, xs)) -> Split m n xs | @cons _ x' n' xs'' => (S n', cons x' xs'') = (Peano.plus m n, xs) -> Split m n xs end) with | nil => _ | cons x xs => _ end). simpl. destruct m as [|m']. + simpl. simplify *. simpl. apply (append nil nil). + simpl. simplify *. + destruct m as [|m']; simpl. simplify *. simpl. apply (append nil (x |: _ :| xs)). simplify *. simpl. specialize (IH _ _ xs). destruct IH. refine (append (cons x xs) ys). + rewrite (eta_vector (fun nv v => (nv, v) = (Peano.plus m n, xs) -> Split m n xs)) in X0. apply (X0 eq_refl). Defined.
imports: Program Bvector List Relations Equations.Prop.Equations Utf8 Arith Wf_nat Vectors.Vector