]
qed.
+(* 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.
+
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate ā¦):