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`.

Fixes new Coq master warning deprecated-hint-without-locality.

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).

This follows iris!387
This closes issue #54.

The name made no sense and it was not used anywhere to my knowledge. If it
was used anywhere, it would be very unreliable as it contained hints like
`rtc_trans` that would generally lead to loops.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

This generalizes Fix_unfold to a setoid setting. In particular,
we can use this to unfold multi-argument fixpoints without
requiring functional extensionality.