A regression on a simple subtyping check on functions

```
module Test
assume val dec : x:int -> Pure int
(requires True)
(ensures (fun y -> y = x - 1))
assume val inc : x:int -> Pure int
(requires True)
(ensures (fun y -> y = x + 1))

let compose (f:'b -> 'c) (g:'a -> 'b) (x:'a) = f (g x)

let ex3 : i:int -> Pure int
(requires (0 <= i))
(ensures (fun j -> 0 <= j))
= compose inc dec
```

This program successfully verified with commit 65fe240; but it fails with 46ce23b (the current master).

Haven't tried to bisect yet to find what caused the regression.