+
+(* Basic constructions with proj_path ***************************************)
+
+lemma lift_path_d_empty_sn (f) (n):
+ ๐ฑโจf@โจnโฉโฉโ๐ = โ[f](๐ฑโจnโฉโ๐).
+// qed.
+
+lemma lift_path_d_lcons_sn (f) (p) (l) (n):
+ โ[fโ๐ฎโจninj nโฉ](lโp) = โ[f](๐ฑโจnโฉโlโp).
+// qed.
+
+(* Basic constructions with proj_rmap ***************************************)
+
+lemma lift_rmap_d_empty_sn (f) (n):
+ f = โ[๐ฑโจnโฉโ๐]f.
+// qed.
+
+lemma lift_rmap_d_lcons_sn (f) (p) (l) (n):
+ โ[lโp](fโ๐ฎโจninj nโฉ) = โ[๐ฑโจnโฉโlโp]f.
+// qed.
+
+lemma lift_rmap_L_sn (f) (p):
+ โ[p](โซฏf) = โ[๐โp]f.
+// qed.
+
+lemma lift_rmap_A_sn (f) (p):
+ โ[p]f = โ[๐โp]f.
+// qed.
+
+lemma lift_rmap_S_sn (f) (p):
+ โ[p]f = โ[๐ฆโp]f.
+// qed.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_lift (Q:predicate โฆ):
+ Q ๐ โ
+ (โn. Q ๐ โ Q (๐ฑโจnโฉโ๐)) โ
+ (โn,l,p. Q (lโp) โ Q (๐ฑโจnโฉโlโp)) โ
+ (โp. Q p โ Q (๐โp)) โ
+ (โp. Q p โ Q (๐โp)) โ
+ (โp. Q p โ Q (๐ฆโp)) โ
+ โp. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p
+elim p -p [| * [ #n * ] ]
+/2 width=1 by/
+qed-.