Prove more equivalences for closure operators on relations.

Add and extend equivalences between closure operators:

• Add ↔ lemmas that relate rtc, tc, nsteps, and bsteps.
• Rename → lemmas rtc_nsteps → rtc_nsteps_1, nsteps_rtc → rtc_nsteps_2, rtc_bsteps → rtc_bsteps_1, and bsteps_rtc → rtc_bsteps_2.
• Add lemmas that relate rtc, tc, nsteps, and bsteps to path representations as lists.

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