Introduce bi_nsteps and add timeless results for bi closures
This MR adds lemmas to show that bi_tc R
and bi_rtc R
are Timeless
whenever R
itself is Timeless
.
It does so by introducing bi_nsteps
, which are n
-step R
reductions, and using its equivalences with bi_tc
and bi_rtc
.