Extend the stratification checker to complain about higher-order arguments

The following definitions now cause warnings:

    Define bad : prop -> prop by
      bad P := bad P -> false.

    Define ugly : prop by
      ugly := (ugly -> false) -> false.

    Define not : prop -> prop by
      not P := P -> false.

    Define r1 : prop -> prop by
      r1 P := P.  /* no warning here */

    Define r2 : prop -> prop by
      r2 P := r1 P -> false.

The compile-time flag Abella.stratification_warnings_are_errors
can be used to turn stratification warnings into errors. Currently
this is set to "false" for backwards compatibility.
Merge pull request #28 from chaudhuri/ho_stratification

Extend the stratification checker to complain about higher-order arguments