-lemma tls_unwind2_rmap_d_sn (f) (p) (m) (n):
- ⇂*[m+n]▶[f]p ≗ ⇂*[m]▶[f](𝗱n◗p).
-#f #p #m #n
-<unwind2_rmap_d_sn >nrplus_inj_dx
+lemma tls_unwind2_rmap_d_dx (f) (p) (h) (k):
+ ⇂*[h+k]▶[f]p ≗ ⇂*[h]▶[f](p◖𝗱k).
+#f #p #h #k
+<unwind2_rmap_d_dx >nrplus_inj_dx