proposition: Lemma split_vapp : ∀ (X : Type) m n (v : vector X m) (w : vector X n), let 'append v' w' := split (vapp v w) in v = v' /\ w = w'.
proof: Proof. intros. funelim (vapp v w); simp split; trivial; auto. destruct split; simp split. dependent elimination X as [pair idpath idpath]. split; constructor. Qed.
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