Proof complexity of two directions of equivalency?

This fits in the program of reverse mathematics. For instance: a subtree of the set of all finite binary strings has an infinite path iff it is infinite. One direction is provable in RCA $_0$ and the other is not.

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$.