update in ground

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind2_rmap_head.ma

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 7b568dc8681403e78308694f011135ba0dcf6175..416c6e7924650b412ad854cb119265877fe14151 100644 (file)
--- 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.