Added the ATP-pragma.

{-# ATP role name [h1 ... hn] #-}

The ATP-pragma indicates that the name and h1, ..., hn, will be used
with an (external) automatic theorem prover (ATP).

The possible roles are: axiom, definition, hint and prove.

It is possible to use the ATP-pragma in conjuction with an external
program called Apia to prove first-order formulae written in Agda
using ATPs. See https://github.com/asr/fotc.