Prove more equivalences for closure operators on relations.

As part of this: turn `rtc_nsteps` and `rtc_bsteps` into ``s.

The `_list` lemmas were proposed by @jules and he provided an initial proof specific to `rtc`.