(* Basic constructions with proj_rmap ***************************************)
+lemma lift_rmap_empty (f):
+ f = โ[๐]f.
+// qed.
+
lemma lift_rmap_d_sn (f) (p) (n):
โ[p](fโ๐ฎโจninj nโฉ) = โ[๐ฑnโp]f.
#f * // qed.
]
qed.
+(* 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.
+
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate โฆ):