-
Robbert Krebbers authored
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`.40a0487a
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`.