partial commit in delayed_updating

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

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 6a52ef2e55cc50dd75b67c906fde312b76156bbc..0d949e3b58d1610f63b9af796044c9cc69fc2c84 100644 (file)
--- 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.