Implement disjoint namespaces for variables and effect names.

This branch extends the syntax of the calculus defined in lang.v with support for two-sorted binders. One sort is reserved for variables that bind values, and the other sort is reserved for effect names that bind labels. The motivation for this change is that it allows the simplification of the typing rules stated in lang.v. Here is an overview of the changes:

• Introduction of the type bsort of sorts.
• Modification of the constructs Var, Rec, and RecV, which now carry a sort.
• Modification of the subst function. Now, this function is parameterised by a sort indicating if the target of the substitution is either a variable or an effect name.
• Reformulation of the typing rules. Now, there is no need for the side conditions ensuring that variable do not mix with effect names.