Terminating expressions

A fix for #129.

See `tests/pos/GeneralizedTermination.hs` and `tests/pos/Even0.hs` as examples.

Some implementation info:
In the example, 
```
 foo :: Int -> Int -> Int
 {-@ foo :: x:Nat -> y:Nat -> Nat /[x+y] @-}
 
 foo n m 
   | cond 1 = 0
   | cond 2 && n > 1 = foo (n-1) m
   | cond 3 && m > 2 = foo (n+1) (m-2)
```

We need to give `foo` a type that checks that `n - 1 + m < n + m`
So I defined a new type
```
RRTy r t
```
 with meaning "if you prove r you get a type t"
So the inner foo has type 
``` foo :: x:Nat -> y:Nat -> RRTy (x+y<n+m) Nat ```

To handle this type there is a new subtyping costraint
`SubR γ r` <=> γ |- r <=> true => true

A nice consequence of having this different kind of constraints is that when they fail we can provide a "more precise" warning. See `tests/neg/GeneralizedTermination.hs` that returns:
```
**** UNSAFE:  Termination Check Error: tests/neg/GeneralizedTermination.hs:9:23-38 
```