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.