+(* Advanced constructions with proj_rmap and path_rcons *********************)
+
+lemma lift_rmap_d_dx (f) (p) (n):
+ (↑[p]f)∘𝐮❨ninj n❩ = ↑[p◖𝗱n]f.
+// qed.
+
+lemma lift_rmap_m_dx (f) (p):
+ ↑[p]f = ↑[p◖𝗺]f.
+// qed.
+
+lemma lift_rmap_L_dx (f) (p):
+ (⫯↑[p]f) = ↑[p◖𝗟]f.
+// qed.
+
+lemma lift_rmap_A_dx (f) (p):
+ ↑[p]f = ↑[p◖𝗔]f.
+// qed.
+
+lemma lift_rmap_S_dx (f) (p):
+ ↑[p]f = ↑[p◖𝗦]f.
+// qed.
+
+lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
+ ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩.
+#f #p #n #m
+<lift_rmap_d_dx <tr_compose_pap <tr_uni_pap //
+qed.
+