Upper bound on the height of terms in proofs with bound-depth-restricted cuts

We prove an upper bound on the height of terms occurring in a most general unifier for the case when the set of term-variables splits to two subsets. A term-variable belongs to the first sub-set iff the depths of all its occurrences coincide, we call such a variable a term-variable of the cut type; otherwise, it belongs to the second sub-set. We bound from above the height of terms occurring in a most general unifier by the number of term-variables of not the cut type and size of the given unification problem. This bound implies an upper bound on the size of terms occurring in proofs in a sequent-style calculus with bound-depth-restricted cuts.