Load "nat.tt"; Data Vect (A:*) : (n:Nat)* = Vnil : (Vect A O) | Vcons : (k:Nat)(a:A)(v:Vect A k)(Vect A (S k)); vec_append : (A:*)(m,n:Nat)(xs:Vect A m)(ys:Vect A n)(Vect A (plus m n)); intros; induction xs; fill ys; intros; fill (Vcons _ _ a v_IH); Qed;