subtyp_ctx_size rule instead of max
updates in narrowing/exp_preserves_sub
termination measure for narrowing/exp_preserves_sub: difference between size of env and max size of env anywhere inside proof tree