transitivity done, with unproven good-bounds assumption
proof ok. deceitful %trustme on good-bounds and sub-tp-refl