idris-0.9.17.1: test/proof009/input

:p arhs
intro x
intros
trivial
qed
:q