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 *. destruct split_struct. depelim xs; intuition. destruct (split_struct (vapp v _)); simpl. intuition congruence. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat Bvector