No need for arbitrary context in subtyping trans.

which is good, because with empty context, we have a shot at proving it.
Add req store_wf to subtp_trans. Looks plausible now.