idris-0.9.13: test/reg042/expected

7