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