nits
done with step_preserves_R

a horrible proof term, a complete pain to write, for an obvious proof