X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_head.ma;h=416c6e7924650b412ad854cb119265877fe14151;hb=41a54a797af98d2867d4bf979d424283fb44a1fc;hp=853f07e9cea4a1ef87954d7cd6e82221d6d26c00;hpb=61bc42e04598a9f5e489c3867af72e700c7fda04;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
index 853f07e9c..416c6e792 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
@@ -89,12 +89,12 @@ lemma unwind2_rmap_head_xap (f) (p) (n):
 ]
 qed.
 
-lemma unwind2_rmap_append_pap_closed (f) (p) (q) (n:pnat):
-      q = ↳[n]q →
-      ♭q = ninj (▶[f](p●q)＠⧣❨n❩).
-#f #p #q #n #Hn
->tr_xap_ninj >(path_head_refl_append p … Hn) in ⊢ (??%?);
->(unwind2_rmap_head_xap_closed … Hn) -Hn
+lemma unwind2_rmap_append_pap_closed (f) (p) (q) (h:pnat):
+      q = ↳[h]q →
+      ♭q = ninj (▶[f](p●q)＠⧣❨h❩).
+#f #p #q #h #Hh
+>tr_xap_ninj >(path_head_refl_append_sn p … Hh) in ⊢ (??%?);
+>(unwind2_rmap_head_xap_closed … Hh) -Hh
 <path_head_depth //
 qed.