A specialization of Gentzen-type deductions and its application

Let $S$ be a sequent, $M$ be some class of formula occurences in $S$ and let $D$ be a proof of $S$ in Gentzen-type system (classical on intuitionistic). A logical inference $L$ in $D$ is said to adjoin to $M$ through the premise $U$ if all side formulas of $L$ in $U$ belong to $M$. $U$ is called then a $M$-premise of $L$. $L$ is said to conform to $M$ if $L$ adjoins to $M$, and all logical inferences above any $M$-premise of $L$ belong to the side formulas of $L$. $D$ conforms to $M$ if all logical inferences adjoining to $M$ conform to $M$.
We prove that under certain rather broad syntactical conditions it is possible to transform every proof into a proof of the same sequent conforming to $M$. The obtained results could be applied to the construction of cut-free variants of some axiomatic theories and to proof procedures for the predicate calculus (classical or intuitionistic).