conjoining term structures

seems to keep equalities we care about (as opposed to previous
version)