Fixed a bug about subordination.

Previously, a term of type T can contain a subterm of type T' only
if T' is subordinate to T. This constraint is applied even if T is not
explicitly closed by the "close" command. With the restriction you
cannot, for example, construct a term of type "ty" that contains
a term of type "tm" using the following signature because "tm" is
not subordinate to "ty":

Kind tm, ty type.
Type app   tm -> tm -> tm.
Type abs   (tm -> tm) -> tm.
Type arr   ty -> ty -> ty.

With this bug fix, the constraint above is checked only if T is closed
explicitly.