wip: subtyping inversion.

by induction on subtyping judgment. barely a bit of the reflexivity
case.
this is going to be painful... need a better strategy.