idris-0.9.9: test/test017/test017a.idr
module scg total vtrans : Vect n a -> Vect n a -> List a vtrans [] _ = [] vtrans (x :: xs) ys = x :: vtrans ys ys
module scg total vtrans : Vect n a -> Vect n a -> List a vtrans [] _ = [] vtrans (x :: xs) ys = x :: vtrans ys ys