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=7b568dc8681403e78308694f011135ba0dcf6175;hpb=084fe5719d41ce13be068050fbade488d4a183ee;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 7b568dc86..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
@@ -93,7 +93,7 @@ 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 p … Hh) in ⊢ (??%?);
+>tr_xap_ninj >(path_head_refl_append_sn p … Hh) in ⊢ (??%?);
 >(unwind2_rmap_head_xap_closed … Hh) -Hh
 <path_head_depth //
 qed.