Implement function input check typing rule for new syntax

[jlvargasme]

let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x * x + y*y

Once the function is called, for example,
let s = add 1 (-.3)

We want to verify that "not ( (x = 1 and y = -3) -> (x < 0 and y < 0))"

In this example, the check should fail since 1 !< 0.