+(* Advanced constructions with proj_rmap and path_rcons *********************)
+
+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.
+