(* 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.