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.