However, I am a little reluctant to add the lemma that you propose, since it is just proved by OBVIOUS. If you have an instance of this lemma in the context of a larger proof where the prover was unable to prove such a step, I'd be interested in hearing about it.