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