solve_proper: add support for subrelation

I realized that solve_proper cannot currently prove things like NonExpansive (λ x, ⌜a = x⌝), which is a bit of a bummer. So this adds the infrastructure required to make that work.