proposition: Lemma split' {X : Type} {m n} (xs : vector X (add m n)) : Split m n xs.
proof: Proof. eassert ?[ty]. revert m n xs. fix IH 3. intros m n xs. refine (match xs as xs' in @vector _ k return (match xs' as xs'' in vector _ n' return Type with | nil => ((0, nil) = (plus m n, xs)) -> Split m n xs | @cons _ n' x' xs'' => (S n', cons x' xs'') = (plus m n, xs) -> Split m n xs end) with | nil => _ | cons n x xs => _ end). destruct m as [|m']. + simpl. simplify *. apply (append nil nil). + simplify *. + destruct m as [|m']; simpl. simplify *. simpl. apply (append nil (x |: n :| xs)). simplify *. simpl. specialize (IH m' n0 xs). rewrite (eta_vector (fun nv (v : vector X nv) => (nv, v) = (plus m' n0, xs) -> Split m' n0 xs)) in IH. specialize (IH idpath). destruct IH. refine (append (cons x xs) ys). + rewrite (eta_vector (fun nv v => (nv, v) = (plus m n, xs) -> Split m n xs)) in X0. apply (X0 idpath). Defined.
imports: Equations(CoreTactics) Equations.HoTT.All Equations.HoTT.WellFounded Coq.Unicode.Utf8 HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Classes.implementations.peano_naturals Equations.HoTT.Tactics