relax wf
tbind <: T2 rule in sub-tp (sensible?)
extend-sub-tp case
extract-sub-tp case
still need to figure out refl and additional trans case