wip
some redundancy to help with proofs. trans-sub-tp tsel2-tsel1 case done. only tbind left.