Added hypothesis and subtype declarations, slight changes to the form of contexts. New syntax for binders: there is no need to add the type for the domain, as it is specified by the type of the variable.