Renamed local_env to var_env, and call_local_env to closure_var_env.
Added simple function subtyping algorithm.
More tests for first-class functions.
Distinguish test cases that Z3 proves wrong from those it cannot prove.
Renamed var_env back into local_env.
Added modulo operation (%).
Added checking of contracts for function casts.
Added README for refined types, and additional test cases.