Add the syntax for quantifiers to value bindings

[gfngfn]

• Add the syntax of explicit type variable binders to let-expressions
• Add the syntax of return type annotations
• Fix how to track MustBeBoundID and MustBeBoundRowID in type environments

-val ~rec lift lf xs =
+val ~rec lift 'a (lf : 'a -> code 'a) (xs : list 'a) : code (list 'a) =
   match xs with
   | []      -> &[]
   | x :: xs -> &(~(lf x) :: ~(lift lf xs))
   end