Three ways of recognizing essential formulas in sequents

Let $A$ be a formula, $\Gamma\to\Delta$ be a sequent. The formula $A$ is unessential in $A,\Gamma\to\Delta$ if derivability of $A,\Gamma\to\Delta$ implies derivability of $\Gamma\to\Delta$. The paper describes 3 sufficient conditions for a formula to be unessential in classical and intuitionistic predicate calculus. The conditions are applied for proving hereditary unsolvability of these theories:
1) the intuitionistic equality theory with the axiom $\rceil\rceil\forall xy(x=y)$, the scheme
\begin{equation} \forall_\alpha\rceil\rceil A\supset\rceil\rceil\forall_\alpha A \end{equation}
and the scheme
\begin{equation} \rceil A\vee\rceil\rceil A; \end{equation}

2) the intuitionistic monadic predicate calculus with one predicate letter with the axiom the scheme (1) and the scheme (2).