Define subtyping, and prove subtyping for some types.

TODO : functions, sums. But these types need to be redefined properly.