usefulness of cbounds is limited, because

precise subdecs narrowing is used by exp_preserves_sub_pr/case subtyp_trans,
which cannot guarantee  nor , so we cannot pass
any of these two to narrowing, so narrowing cannot get cbounds_ctx for
old env nor for new env

but maybe we can use it to say a type is realizable if it is a supertype of
a cbounds type
all termination measure problems of narrowing are in the case exp_sel
cp dev/cbounds-ip-pr-muDot.v dev/predict-max-ctx-size-ip-pr-muDot.v
some more cbounds stuff + max_ctx_subtyp judgment to predict max size of env in subtype derivations
recursive types in lhs of <: can lead to arbitrarily big environment if rhs of <: is big enough; is this a problem?
cp dev/predict-max-ctx-size-ip-pr-muDot.v dev/max-ctx-size-ip-pr-muDot.v
measure max env size in subtyp judgments