Problem:

To get the termination measure working, the transitivity push-back
proof needs a Lo<:Hi proof inside subtyp_sel_r, so the case sel_r of
simple_narrow_subtyp needs to narrow [has G x L (dec_typ Lo2 Hi2)] to
[has G x L (dec_typ Lo1 Hi1)] in such a way that [Lo1 <: Hi1], so
simple_narrow_has_dec_typ should guarantee that the narrowed dec_typ
still has good bounds, so subdec_typ has to require that [Lo1 <: Hi1],
so decs_bot_has_subdec has to prove Top <: Bot.