X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_eq.ma;h=b93aabf0ffb8316da2e18428b92a6a9b54798acd;hp=c075e2f250e8af9a1642edb561aa6b93186a26f7;hb=829e3a8af3229c4e625245f7265dd67939da98c4;hpb=41a54a797af98d2867d4bf979d424283fb44a1fc

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
index c075e2f25..b93aabf0f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
@@ -28,9 +28,9 @@ lemma unwind2_rmap_eq_repl (p):
 /3 width=1 by preunwind2_rmap_eq_repl/
 qed-.
 
-lemma tls_unwind2_rmap_d_dx (f) (p) (n) (k):
-      ⇂*[n+k]▶[f]p ≗ ⇂*[n]▶[f](p◖𝗱k).
-#f #p #n #k
+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
 /2 width=1 by tr_tls_compose_uni_dx/
 qed.