idea: inversion axiom (rule) and a push-back theorem for it
total expansion: subdecs_typ: require right dec_typ to have good bounds, but not the left one