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