2 include "delayed_updating/unwind1/unwind.ma".
4 include "ground/relocation/tr_compose_compose.ma".
5 include "ground/relocation/tr_compose_eq.ma".
7 (* Advanced constructions with proj_rmap and stream_tls *********************)
9 lemma unwind_rmap_tls_d_dx (f) (p) (m) (n):
10 ⇂*[m+n]▼[p]f ≗ ⇂*[m]▼[p◖𝗱n]f.
12 <unwind_rmap_d_dx >nrplus_inj_dx
13 /2 width=1 by tr_tls_compose_uni_dx/