Type checking ./interactive003.idr ys x :: (app xs ys) [] f x y :: (vzipWith f xs ys)