A coherence theorem for canonical morphisms in cartesian closed categories

A coherence theorem states that any diagram of canonical maps from $A$ to $B$ is commutative, i.e. any two maps from $A$ to $B$ are equal if objects $A,B$ satisfy some natural condition.
We employ familiar translation ([2], [6]) of the canonical maps in cartesian closed category into derivations in ($\&,\supset$)-fragment of intuitionistic propositional calculus. Two maps are equal iff corresponding derivations are equivalent (i.e. they have the same normal form or their deductive terms are equivalent ([2], [5]).
We consider the following form of coherence theorem. If $S$ is a sequent and any propositional variable occurs no more than twice in $S$ then any two derivations of $S$ are equivalent. (It makes no difference to consider cut-free $L$-deductions or normal natural deductions (cf.[9]).)
We give two proofs of the coherence theorem. The first proof (due to A. Babajev) uses the natural deduction system and deductive terms.
The second proof (due to S. Solovaov) uses a reduction of the formula depth [7] and Kleene's results on permutability of inferences in Gentzen's calculi LK and LJ.