/*

  For any value type `T`, the term `=>T` is the type of computations that
  compute values of type `T` whenever they terminate normally.
  
  For any subtypes `S`, `T` of `values`, `S=>T` is the type of computations
  that compute values of type `T` whenever they terminate normally, and
  either do not refer at all to the `given` entity, or require the `given`
  entity to have type `S`.