Invariants

Enable checkable invariants (ie., at each call of a data-constructor LH proves that the invariant holds) via "using" annotation:

~~~
{-@ using (F a) as  {v : F a | (fy v) = (fx v) } @-}
~~~

See:
[tests/pos/Invariants.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/invariants/tests/pos/Invariants.hs) and [tests/neg/Invariants.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/invariants/tests/neg/Invariants.hs)