proposition: Lemma split_struct_vapp : ∀ (X : Type) m n (v : vector X m) (w : vector X n), let 'append v' w' := split_struct (vapp v w) in v = v' /\ w = w'.
proof: Proof. intros. funelim (vapp v w); simp split_struct in *; try easy. destruct (split_struct (v ++v w)); simpl. dependent elimination X as [pair idpath idpath]; easy. 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