X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_structure.ma;h=0d949e3b58d1610f63b9af796044c9cc69fc2c84;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=6a52ef2e55cc50dd75b67c906fde312b76156bbc;hpb=5c2d38b46908f662cbb717156b29101ff30f8352;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
index 6a52ef2e5..0d949e3b5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
@@ -17,15 +17,16 @@ include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_depth.ma".
 include "ground/relocation/tr_pushs.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
 (* Constructions with structure and depth ***********************************)
 
-lemma unwind2_rmap_structure (p) (f):
+lemma unwind2_rmap_structure (f) (p):
       (⫯*[♭p]f) = ▶[f]⊗p.
-#p elim p -p //
-* [ #n ] #p #IH #f //
-[ <unwind2_rmap_A_sn //
-| <unwind2_rmap_S_sn //
+#f #p elim p -p //
+* [ #k ] #p #IH //
+[ <unwind2_rmap_L_dx //
+| <unwind2_rmap_A_dx //
+| <unwind2_rmap_S_dx //
 ]
 qed.