include "delayed_updating/substitution/lift.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_pushs.ma".
include "ground/arith/nat_pred_succ.ma".
(* LIFT FOR PATH ***********************************************************)
(* Basic constructions with structure and depth ****************************)
lemma lift_rmap_structure (p) (f):
- (⫯*[â\86\93â\9d\98pâ\9d\98]f) = â\86\91[â\8a\97p]f.
+ (⫯*[❘p❘]f) = ↑[⊗p]f.
#p elim p -p //
* [ #n ] #p #IH #f //
-[ <lift_rmap_L_sn <IH -IH >tr_pushs_swap //
-| <lift_rmap_A_sn //
+[ <lift_rmap_A_sn //
| <lift_rmap_S_sn //
]
qed.