I think that there are numerous trivial examples of this.

Take any implication $p\to q$ that is provable, but has no very short proof. It follows that the equivalence $$q\leftrightarrow (p\vee q)$$ is also provable, and furthermore has a trivial proof in the forward direction, but no very proof in the converse direction, since any such proof also gives a very short proof that $p\to q$.

I think that there are numerous trivial examples of this.

Take any implication $p\to q$ that is provable, but has no short proof. It follows that the equivalence $$q\leftrightarrow (p\vee q)$$ is also provable, and furthermore has a trivial proof in the forward direction, but no very short proof in the converse direction, since any such proof also gives a short proof that $p\to q$.